diff options
| author | yoni206 <yoni206@users.noreply.github.com> | 2019-10-03 15:23:58 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-03 15:23:58 -0700 |
| commit | 167947ab81094de28251bb885c8cf84e7168c43b (patch) | |
| tree | 385bc47f48611c535309721c8b933f3117a2e9ed /test/regress/regress0/proof_no_support.smt2 | |
| parent | 76ddd08e3805ca262d732ce78db165272ef0852e (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.
Diffstat (limited to 'test/regress/regress0/proof_no_support.smt2')
| -rw-r--r-- | test/regress/regress0/proof_no_support.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress0/proof_no_support.smt2 b/test/regress/regress0/proof_no_support.smt2 new file mode 100644 index 000000000..3d19a109e --- /dev/null +++ b/test/regress/regress0/proof_no_support.smt2 @@ -0,0 +1,21 @@ +;COMMAND-LINE: --check-proofs +;EXIT: 1 +;EXPECT: (error "Error in option parsing: Proofs are only supported for sub-logics of QF_AUFBVLIA.") +(set-logic ALL) + +(declare-const a Int) + +(assert (and + (= + a + (* a a) + ) + (not (= a 0)) + (not (= a 1)) + ) +) + +(check-sat) + + + |