z3 performance issue #5057
-
|
For smt2-lib file: stuck2.smt.txt , I find that it's very slow (1.5 s) on z3, but it run instantaneous on cvc4. Will setting theory or strategy in z3 helps? If so, what should I set? In the constraints generated and dumped, i see a lot of intermediate variable being created. Could that be the cause? Or in general looking at the smt2-lib file, is there anything I can do to speed up z3 performance? |
Beta Was this translation helpful? Give feedback.
Replies: 1 comment
-
|
they are let-bound variables, not intermediate variables |
Beta Was this translation helpful? Give feedback.
they are let-bound variables, not intermediate variables
set the option smt.arith.solver=2, or in the file (set-option :smt.arith.solver 2) and it is much faster.
This is an instance where the new arithmetical solver suffers from a performance overhead not shared with the legacy arithmetic solver.