Sep 20, 2013 at 3:34 PM
Edited Sep 20, 2013 at 3:41 PM
I have an instance which could be very efficiently solved by old version of Z3(version 2.18). It return SAT in a few seconds.
However, when I try it on the current version of Z3(version 4.3.1). It does not return any result after 10 minutes.
Here are some details about the experiment. Could anybody give some advice?
There are about 50,000 lines in the smt file, so I can not post it here. I would be happy to send the file if anybody are interested.
- there are 4000 Bool variables and 200 Int variables
- all the constraint are in propositional logic with comparison between integers like a < b
- platform: open suse linux 12.3@thinkpad T400s
- Z3 v2.18 was downloaded as a linux binary last year (I cannot find the link now)
- Z3 v4.3.1 was downloaded as source code, and I compile it on my laptop by using the default setting