supposed be UNSAT, but it is SAT
how to run?
./hifrog --logic prop --unwind 10
#1 Updated by Karine Even Mendoza over 1 year 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?