projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 5490607) | patch
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled...
authoryoni206 <yoni206@users.noreply.github.com>
Fri, 20 Apr 2018 22:07:55 +0000 (15:07 -0700)
committerGitHub <noreply@github.com>
Fri, 20 Apr 2018 22:07:55 +0000 (15:07 -0700)
commiteddacee2d28846089e6dd356f72e6d39a371ec0f
tree18cf46f985b656a75aea80074bd956d8f6826627tree
parent549060790c9e91d9fc37b882e137bb36e5b538eacommit | diff
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled (#1801)

Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.
src/smt/smt_engine.cpp diff | blob | history
src/theory/bv/theory_bv.cpp diff | blob | history
test/regress/Makefile.tests diff | blob | history
test/regress/regress0/bv/bv-options1.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv-options2.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv-options3.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv-options4.smt2 [new file with mode: 0644] blob
test/regress/run_regression.py diff | blob | history