summaryrefslogtreecommitdiff
path: root/test/regress/regress1/quantifiers
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress1/quantifiers')
-rw-r--r--test/regress/regress1/quantifiers/Makefile.am3
-rw-r--r--test/regress/regress1/quantifiers/set3.smt21
2 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress1/quantifiers/Makefile.am b/test/regress/regress1/quantifiers/Makefile.am
index 159f2e088..af277af90 100644
--- a/test/regress/regress1/quantifiers/Makefile.am
+++ b/test/regress/regress1/quantifiers/Makefile.am
@@ -80,7 +80,8 @@ TESTS = \
RNDPRE_4_1-dd-nqe.smt2 \
set8.smt2 \
z3.620661-no-fv-trigger.smt2 \
- arith-rec-fun.smt2
+ arith-rec-fun.smt2 \
+ set3.smt2
# removed because they take more than 20s
# javafe.ast.ArrayInit.35.smt2
diff --git a/test/regress/regress1/quantifiers/set3.smt2 b/test/regress/regress1/quantifiers/set3.smt2
index d3e51d996..bd208c6d3 100644
--- a/test/regress/regress1/quantifiers/set3.smt2
+++ b/test/regress/regress1/quantifiers/set3.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --full-saturate-quant
(set-logic AUFLIA)
(set-info :source | Assertion verification of simple set manipulation programs. |)
(set-info :smt-lib-version 2.0)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback