projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 76ddd08) | patch
Disable proofs for unsupported logics (#3327)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 3 Oct 2019 22:23:58 +0000 (15:23 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Thu, 3 Oct 2019 22:23:58 +0000 (15:23 -0700)
commit167947ab81094de28251bb885c8cf84e7168c43b
tree385bc47f48611c535309721c8b933f3117a2e9edtree
parent76ddd08e3805ca262d732ce78db165272ef0852ecommit | diff
Disable proofs for unsupported logics (#3327)

This commit makes CVC4 complain if the user asked for proofs for an unsupported logic (in this contest, ALL is considered unsupported).
Changes in the regression script are introduced as well, in order to only request proofs for regressions in supported logics.
src/smt/smt_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/proof_no_support.smt2 [new file with mode: 0644] blob
test/regress/run_regression.py diff | blob | history