I want to solve a set of constraints as follows:
C1: x1 > x2
C2: y1 = x1 + t1
C3: y2 = x2 + t2
C4: 2 <= t1 <= 7
C5: 5 <= t2 <= 9
C6: x1 >= 0
C7: x2 >= 0
C8: y1 < y2
If I normally check this in Z3, it will provide me a satisfiable solution. But I want to know whether the set of constrains are true for all values of t1 and t2.
How can I model that in Z3 or any other SMT solver?
Your question is rather ambiguous, as it can be interpreted to mean different things. But I gather you're trying to establish if there are values that can violate the implication of these constraints? That is, in your example, is there a way to pick values such that C1-C7 are all satisfied but not C8?
If that's the case, then the usual trick is to identify what fact you want to follow from the other facts your constraints present. Then, you assert the negation of the conclusion. If the negation is unsatisfiable, then your constraints are valid for all possible assignments. If you get unsat, however, then that means there are no counter-examples, i.e., your constraints are valid for all possible assignments.
In your case, I'd consider C1-C7 to be "given" and C8 is what you're trying to establish. You simply assert all of C1-C7, but negation of C8. In the following, I'm assuming variables are integer values:
(set-logic ALL)
(set-option :produce-models true)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(declare-fun y1 () Int)
(declare-fun y2 () Int)
(declare-fun t1 () Int)
(declare-fun t2 () Int)
(assert (> x1 x2)) ; C1
(assert (= y1 (+ x1 t1))) ; C2
(assert (= y2 (+ x2 t2))) ; C3
(assert (<= 2 t1 7)) ; C4
(assert (<= 5 t2 9)) ; C5
(assert (>= x1 0)) ; C6
(assert (>= x2 0)) ; C7
(assert (not (< y1 y2))) ; NEGATION of C8
(check-sat)
(get-value (x1 x2 t1 t2 y1 y2))
When run, z3 says:
sat
((x1 1)
(x2 0)
(t1 4)
(t2 5)
(y1 5)
(y2 5))
So, there you go. Your constraints are not valid for the above choices, as you can easily verify yourself.
Is this what you're looking for?