summaryrefslogtreecommitdiff
path: root/test/regress/regress2
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2019-09-18 15:03:12 -0500
committerGitHub <noreply@github.com>2019-09-18 15:03:12 -0500
commita9c40f60e4b36494e10520dcc3a3985b4700342f (patch)
tree70dc9c73b5ce2007850ab40e623a55d205ba62e4 /test/regress/regress2
parent40b83fd9205a7eb772a2ac413f8a3641db1fb02c (diff)
Decouple fmf-bound and finite-model-find (#3297)
Diffstat (limited to 'test/regress/regress2')
-rw-r--r--test/regress/regress2/quantifiers/net-policy-no-time.smt21
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress2/quantifiers/net-policy-no-time.smt2 b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
index 6dcb47201..938aa01ea 100644
--- a/test/regress/regress2/quantifiers/net-policy-no-time.smt2
+++ b/test/regress/regress2/quantifiers/net-policy-no-time.smt2
@@ -1,5 +1,6 @@
(set-logic UFDTLIRA)
(set-option :fmf-bound true)
+(set-option :finite-model-find true)
(set-option :produce-models true)
(set-info :status sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback