supposed be UNSAT, but it is SAT
how to run?
./hifrog --logic prop --unwind 10
#1 Updated by Karine Even Mendoza 12 months ago
The problem is in propositional logic, we get SAT and not UNSAT
The SSA encoding is valid and gives UNSAT in z3, not sure where is the problem.
I attached the SSA dump here.
How can we get a dump from OpenSMT to test what is the input to OpenSMT?