I have the z3py code snippet below
I = Int('I')
x = Int('x')
a = Int('a')
O = Bool('O')
constraint1 = Implies(x==0,O)
constraint2 = Implies(And(x >= 6, O), x ==6)
test = And(constraint1,constraint2,(O == I <= a), I==x)
s = Solver()
s.add(ForAll([x],test))
result = s.check()
print result
if result == sat:
print s.model()
It needs to infer the correctness of the invariant O via a set of connections provided. In this case I have provided the connection I == x so all z3 has to do is guess the constant a as 6 to give to give the correct invariant of O == (x <= 6) which satisfies the horn clauses. However I keep getting UNSAT. Any idea why?
The constraints are unsat.
You have a formula of the form Forall x . And(.... , I == x) The last conjunction implies Forall x . I == x, which is unsat because I is drawn from an infinite set of numbers, so it is not the case that every x in this infinite set equals I.