From 61acf8c8d621799984e622b65598caec4acceb52 Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Thu, 14 Jun 2012 14:57:24 +0000
Subject: failing quantifier

---
 test/regress/regress0/decision/Makefile.am           |  1 +
 test/regress/regress0/decision/quant-ex1.smt2        | 12 ++++++++++++
 test/regress/regress0/decision/quant-ex1.smt2.expect |  3 +++
 3 files changed, 16 insertions(+)
 create mode 100644 test/regress/regress0/decision/quant-ex1.smt2
 create mode 100644 test/regress/regress0/decision/quant-ex1.smt2.expect

(limited to 'test')

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
-- 
cgit v1.2.3