migration from yices to Z3

[fclaudel]

Hi

We're considering a move from yices solver to Z3 solver in our solution, as it provides more functionality and integrates well with C++ code.

Initial queries that we've tried appear to take much longer in Z3. This can be reproduced using the z3 and yices Windows tools, using default configuration:
z3.exe -smt2 testcase.smt2 -st
yices-smt2.exe testcase.smt2 --stats

z3 and yices (average on 50 runs) times are reported as 0.01 and 0.00248 respectively on the same machine.

In our solution, yices is configured as follows:
Description of parameters available at https://yices.csl.sri.com/doc/parameters.html
yices_default_config_for_logic (config, "QF_BV"); // use QF_BV logic
yices_set_config (config, "mode", "one-shot"); // only one call to the check operation allowed
yices_set_param (params, "fast-restart", "true"); // fast restart heuristics
yices_set_param (params, "c-factor", "1.1"); // increase factor for c-threshold after every restart
yices_set_param (params, "d-factor", "1.1"); // secondary threshold used only if fast-restart is true
yices_set_param (params, "randomness", "0"); // fraction of random decisions in branching
yices_set_param (params.get (), "branching", "positive"); // always set selected decision variable to true

Is there an equivalent configuration in Z3 that would help bridge the gap in runtime?
Any advice is much welcome.
testcase.smt2.txt

[ThomasHaas]

I don't have an answer to your question but I will add to it.
We use SMT solvers to do program verification and we noticed that Yices2 (default settings, incremental) often outperforms all other SMT solvers (also default settings) by sometimes even an order of magnitude. Some benchmarks even take multiple hours for Z3 whereas Yices2 can do them in 10 minutes.
I asked the Yices2 developers if they have an idea on why that is (Link), but I haven't got any answers yet. Maybe Nikolaj has an idea on what magic Yices2 uses to be so fast though :)

[fclaudel]

Thanks @ThomasHaas for your comment.

@NikolajBjorner would you have some advice on z3 configuration to try out?
If performance gap could be reduced through configuration, that may be acceptable in our solution given the other benefits such as FP handling.