summaryrefslogtreecommitdiff
path: root/test/regress/regress0/quantifiers/ex7.smt2
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/quantifiers/ex7.smt2')
-rw-r--r--test/regress/regress0/quantifiers/ex7.smt21
1 files changed, 1 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/ex7.smt2 b/test/regress/regress0/quantifiers/ex7.smt2
index 0cac5ff54..11a83fdc4 100644
--- a/test/regress/regress0/quantifiers/ex7.smt2
+++ b/test/regress/regress0/quantifiers/ex7.smt2
@@ -9,4 +9,5 @@
(declare-fun f (U) U)
(assert (and (= a b) (forall ((x U)) (=> (or (= (f x) c) (= x a)) (= x b)))))
(check-sat)
+(get-info :reason-unknown)
(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback