Question: Fallback from SMTInterpol to Z3/CVC4 when bit-vector terms are present in Boogie inputs

[martin-neuhaeusser]

We have many Boogie models where some tiny aspects are encoded using bit-vector terms and most of the model is using integer theory terms.

When we run trace abstraction with strategy Penguin (or others) on those files, SMTInterpol throws an exception and errors out. That exception remains uncaught and terminates Ultimate Automizer. Is there a setting somewhere that could be used to make trace abstraction gracefully handle that exception (similar to those that are raised when SMTInterpol finds non-linear arithmetic operators) by falling back to other SMT solvers?

If that's not possible, I can share a patch that tries to add this "feature" (if it is actually desired).

[Heizmann]

Thanks for the hint.

So far, our Boogie files had either integer or bitvectors but never both. But we definitely want to support the combination.

Regarding your question: If you use the following setting Ultimate Automizer will fall back to other SMT solvers on all exceptions. /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction/Trace\ refinement\ exception\ blacklist=NONE However, I am very reluctant to use this setting because it may hide fixable bugs that occur only in combination with one specific SMT solver.

I have a, yet immature, plan that would also fix your problem. I want to implement a wrapper around SMTInterpol that overapproximates unsupported terms by true and returns unknown instead of sat if something was overapproximated. The benefit of this would be that we could still get unsat results from SMTInterpol, e.g., in cases were non-linear arithmetic or bitvectors only play a minor role.

[martin-neuhaeusser]

That sounds very good. We have some low-level aspects of our global state that is best represented as a bit-vector; but they are rarely used, if at all. So in many of our cases, any overapproximation would potentially do the job. Thanks for the explanation!