3 ms·
That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formu
by OxO4 8y ago
That actually depends on the logic being used. Some of the logics supported by Z3 are not even decidable. In fact, even solving quantifier-free bit-vector formulas is NEXPTIME-complete [0] when using a binary encoding.
[0] http://smt2012.loria.fr/paper7.pdf http://smt2012.loria.fr/paper7.pdf
- schoen 8y agoThanks for the clarification! What do Z3 and other SMT solvers do if you ask them about undecidable questions? Do they potentially run forever?