diff options
| author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-04-16 17:09:46 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-16 17:09:46 -0700 |
| commit | 3d527f54dd3eacd8c3a7ff3bdec8f29844884e2c (patch) | |
| tree | 129696183248319db5061904c7b2566ad51533a3 | |
| parent | ea11c2dc36e13b2c150161cf6b1bc052e2685261 (diff) | |
| parent | a66a1915cb12faa18ac806d83b4fc2aae18426aa (diff) | |
Merge branch 'master' into d_slow_regd_slow_reg
| -rw-r--r-- | test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect | 2 | ||||
| -rw-r--r-- | test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 | 1 |
2 files changed, 2 insertions, 1 deletions
diff --git a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect index 7fd1d5a98..9d6ac53ca 100644 --- a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect +++ b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2.expect @@ -1,2 +1,2 @@ -% COMMAND-LINE: --decision=justification +% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification % EXPECT: unsat diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 index 6acf4a3c6..6465e27d6 100644 --- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 +++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 @@ -1,3 +1,4 @@ +; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores (set-logic AUFLIRA) (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods. |