failing quantifier

diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am
index e443d72011a2ccbd595d439488254d7b56609a69..1cc6052271b1577dd362eb2f9d43dcca6a2808b3 100644 (file)
--- 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 (file)
index 0000000..a8f4ff2
--- /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 (file)
index 0000000..66f5e51
--- /dev/null
+++ b/test/regress/regress0/decision/quant-ex1.smt2.expect
@@ -0,0 +1,3 @@
+% COMMAND-LINE: --decision=justificationo
+% EXPECT: unknown (INCOMPLETE)
+% EXIT: 0