From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 14 Jun 2012 14:57:24 +0000 (+0000)
Subject: failing quantifier
X-Git-Tag: cvc5-1.0.0~8020
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=61acf8c8d621799984e622b65598caec4acceb52;p=cvc5.git

failing quantifier
---

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index e443d7201..1cc605227 100644
--- a/test/regress/regress0/decision/Makefile.am
+++ b/test/regress/regress0/decision/Makefile.am
@@ -24,6 +24,7 @@ TESTS =	\
 
 # Incorrect answers:
 #	aufbv-fuzz01.smt \
+#	quant-ex1.smt2 \
 #
 
 EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/decision/quant-ex1.smt2 b/test/regress/regress0/decision/quant-ex1.smt2
new file mode 100644
index 000000000..a8f4ff2b9
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.smt2
@@ -0,0 +1,12 @@
+(set-logic AUFLIRA)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status sat)
+(declare-sort U 0)
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun f (U) U)
+(declare-fun p () Bool)
+(assert (and (= a b) (forall ((x U)) (=> (and (= (f x) a) (not (= (f x) b))) p))))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/decision/quant-ex1.smt2.expect b/test/regress/regress0/decision/quant-ex1.smt2.expect
new file mode 100644
index 000000000..66f5e51ba
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.smt2.expect
@@ -0,0 +1,3 @@
+% COMMAND-LINE: --decision=justificationo
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0