Major performance difference between Yices2 and Z3 on BV benchmarks #492
Description
The following is not an issue (at least not for Yices2) but rather a question I'm curious about.
We do program verification using incremental SMT solving where we encode the program's dataflow using either integers or BVs.
We make the following observation:
(1) Z3 on integer encodings is generally faster than Z3 on BV encodings (assuming the program uses only arithmetic and no bitwise operations)
(2) Yices2 on BV encodings is generally faster than Yices2 on integer encodings (i.e., the opposite of Z3). Furthermore, on BVs it is around an order of magnitude faster than Z3 (and other SMT solvers IIRC).
In particular, I'm curious about why Yices2 is so fast on BV encodings. Do you happen to know what technique is implemented in Yices2 that makes it so much faster than Z3? Is it the MCSAT approach of Yices2 or perhaps just better rewriting/preprocessing/inprocessing?