projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5d0a5a7) | patch
Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)
authorAndres Noetzli <andres.noetzli@gmail.com>
Sat, 16 Mar 2019 06:23:06 +0000 (06:23 +0000)
committerGitHub <noreply@github.com>
Sat, 16 Mar 2019 06:23:06 +0000 (06:23 +0000)
commit192aa1b5d98ca1a0a2c5e5c8ec603ebb9d14d261
tree02d53553529fcfe5cb43bca77abcbaf906309072tree
parent5d0a5a729680a1db3f44e31037955390e86440cecommit | diff
Limit --solve-int-as-bv=X to QF_NIA/QF_LIA/QF_IDL (#2868)

Fixes #1715. We do not support the `--solve-int-as-bv=X` preprocessing
pass with logics other than pure QF_NIA/QF_LIA/QF_IDL. This commit adds
a corresponding check and throws an option exception if an incompatible
logic has been set.
src/smt/smt_engine.cpp diff | blob | history