summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-02-17 13:29:09 -0600
committerGitHub <noreply@github.com>2020-02-17 13:29:09 -0600
commit6a761852b93510bf707e7002ad663ca0f36ad720 (patch)
treea91cbd198e21e78b40ce7d6a943db962ee0c30c1 /test/regress
parentb19c08997e15d2e42f61f1936fd60c5e34081d68 (diff)
Option to limit the number of rounds of enumerative instantiation (#3760)
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/regress1/quantifiers/issue3481.smt22
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress1/quantifiers/issue3481.smt2 b/test/regress/regress1/quantifiers/issue3481.smt2
index 47d2bcbe4..fe8c84d62 100644
--- a/test/regress/regress1/quantifiers/issue3481.smt2
+++ b/test/regress/regress1/quantifiers/issue3481.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --full-saturate-quant
+; COMMAND-LINE: --full-saturate-quant --full-saturate-quant-limit=2
; EXPECT: unsat
;; produced by cvc4_16.drv ;;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback