search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Performance regression when using const_array #77

Closed mikhailramalho closed 4 years ago

mikhailramalho commented 4 years ago

We generate the following two formulas:

  1. Using const_array: const_array.trace.txt

  2. Using array array.trace.txt and initializing all the positions with a default value.

While the latter is solved in 1s, the former is running for more than 30 minutes now.

mpreiner commented 4 years ago

Thanks for pointing out! This was due to a missing case for const arrays in the rewriter. Fixed with d46fb7b. Let us know if you run into any other problems.

mikhailramalho commented 4 years ago

Everything seems to be working flawlessly now, thanks!

I'm eagerly waiting for the new version!