summaryrefslogtreecommitdiff
path: root/test/regress/regress1
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-03-10 18:40:29 -0500
committerGitHub <noreply@github.com>2020-03-10 16:40:29 -0700
commit130963b0ffa5850d59b1bff9ad82c63703600097 (patch)
treeef1882f492d6b6bc325e7a2e8af0b59d977cace3 /test/regress/regress1
parentd55bad95755c089adaac69bce106787425b56029 (diff)
Fix options for regression: --sort-inference is incompatible with unsat cores. (#4011)
Diffstat (limited to 'test/regress/regress1')
-rw-r--r--test/regress/regress1/issue3990-sort-inference.smt22
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/regress1/issue3990-sort-inference.smt2 b/test/regress/regress1/issue3990-sort-inference.smt2
index f048718a8..5d036a84f 100644
--- a/test/regress/regress1/issue3990-sort-inference.smt2
+++ b/test/regress/regress1/issue3990-sort-inference.smt2
@@ -1,3 +1,5 @@
+; COMMAND-LINE: --sort-inference --no-check-unsat-cores
+; EXPECT: unsat
(set-logic ABV)
(set-option :sort-inference true)
(set-info :status unsat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback