I wanted to test whether the assert statement holds for z3 results.
To do so, I test the following statement: exists an integer x, such that for all integers y, (x>y). Which is false: there is no integer greater than the rest of the integers.
So I translate this to Z3py:
y_1 = Int('y_1')
x_1 = Int('x_1')
ttt = Tactic("qe")
w = Goal()
phi = Exists(x_1, ForAll (y_1, (x_1>y_1)))
w.add(phi)
result_ttt = ttt(w)
print(result_ttt)
As expected, the printed result is: [[False]]
So I test assert the following:
assert [[False]] == result_ttt
And, surprisingly, the result is assertion error!
Any help? Probably it has to do with the type of result_ttt being <class 'z3.z3.ApplyResult'> (after doing type(result_ttt).
Note that, analogously, if we choose a satisfiable statement the assertion does not hold either.
The chosen statement has been: for all integers x, exists integer y, (x>y). Which is true. In this case, the result is [[]] (since quantifier elimination is satisfactory). And when doing assert [[]] == result the result is negative.
When you write:
[[False]]
all that means is that you've a nested list with that element in it. Note that this has nothing to do with z3. It's a valid Python object.
Compare this to your result_tt, which is a Goal. So, you're trying to compare a Goal to a nested python list; and those two things are never going to be equal. They are completely different objects. Hence the assertion failure.
You're getting confused by the fact that these two things print the same way. But checking equality is an entirely different operation. If you really want to compare that they "print" the same, you can say something like:
assert '[[False]]' == obj_to_string(result_ttt)
But of course that's very ugly and is fragile in case z3 developers decide to change how goals are converted to strings later on.
In general, you shouldn't be trying to compare goals to anything else, and instead use a solver to prove them, or tactics to transform and eliminate them. Using them in any other way will be fragile and will likely not do what you want in the first place to start with.