From 391cfbd3f8e71fd4e9179b983551c5baf7122a94 Mon Sep 17 00:00:00 2001
From: Clark Barrett <barrett@cs.nyu.edu>
Date: Wed, 6 Jun 2012 17:49:51 +0000
Subject: [PATCH] Fixed broken test case, removed one that is a mistake

---
 .../regress0/unconstrained/Makefile.am        |  4 +-
 .../regress0/unconstrained/bvbool3.smt2       |  3 +-
 .../regress0/unconstrained/bvbool3.smt3       | 37 -------------------
 3 files changed, 4 insertions(+), 40 deletions(-)
 delete mode 100644 test/regress/regress0/unconstrained/bvbool3.smt3

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index 984cd4d45..d3adc2167 100644
--- a/test/regress/regress0/unconstrained/Makefile.am
+++ b/test/regress/regress0/unconstrained/Makefile.am
@@ -20,6 +20,7 @@ TESTS =	\
 	arith7.smt2 \
 	arith.smt2 \
 	array1.smt2 \
+	bvbool3.smt2 \
 	bvbool2.smt2 \
 	bvbool.smt2 \
 	bvcmp.smt2 \
@@ -62,8 +63,7 @@ TESTS =	\
 	xor.smt2
 
 # bvbool3 takes too long for regress0
-EXTRA_DIST = $(TESTS) \
-	bvbool3.smt2
+EXTRA_DIST = $(TESTS)
 
 #if CVC4_BUILD_PROFILE_COMPETITION
 #else
diff --git a/test/regress/regress0/unconstrained/bvbool3.smt2 b/test/regress/regress0/unconstrained/bvbool3.smt2
index 6f72246f0..a689804f7 100644
--- a/test/regress/regress0/unconstrained/bvbool3.smt2
+++ b/test/regress/regress0/unconstrained/bvbool3.smt2
@@ -7,6 +7,7 @@
 (declare-fun x2 () (_ BitVec 10))
 (declare-fun x3 () (_ BitVec 10))
 (declare-fun x4 () (_ BitVec 10))
+(declare-fun x5 () (_ BitVec 10))
 (declare-fun p1 () Bool)
 (declare-fun p2 () Bool)
 (declare-fun p3 () Bool)
@@ -20,7 +21,7 @@
   (=
    (a2
     (ite 
-     (=> (or p1 p1) (and (= (bvnor (bvnand (bvor x1 x1) (bvand x0 x0)) x3) ((_ extract 9 0) v3)) p1))
+     (=> (or (= x2 x4) (= x2 x5)) (and (= (bvnor (bvnand (bvor x1 x1) (bvand x0 x0)) x3) ((_ extract 9 0) v3)) p2))
      v2
      6)
     )
diff --git a/test/regress/regress0/unconstrained/bvbool3.smt3 b/test/regress/regress0/unconstrained/bvbool3.smt3
deleted file mode 100644
index 7c9362672..000000000
--- a/test/regress/regress0/unconstrained/bvbool3.smt3
+++ /dev/null
@@ -1,37 +0,0 @@
-(set-logic QF_AUFBVLIA)
-(set-info :source |
-This benchmark demonstrates the need for propagating unconstrained arrays
-and bit-vectors.
-
-Contributed by Robert Brummayer (robert.brummayer@gmail.com)
-|)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(set-info :status sat)
-(declare-fun x0 () (_ BitVec 10))
-(declare-fun x1 () (_ BitVec 10))
-(declare-fun x2 () (_ BitVec 10))
-(declare-fun x3 () (_ BitVec 10))
-(declare-fun x4 () (_ BitVec 10))
-(declare-fun p1 () Bool)
-(declare-fun p2 () Bool)
-(declare-fun p3 () Bool)
-(declare-fun v2 () Int)
-(declare-fun a2 (Int) (_ BitVec 1024))
-(declare-fun v3 () (_ BitVec 1024))
-(declare-fun v4 () (_ BitVec 1024))
-(declare-fun v5 () (_ BitVec 1024))
-(assert
- (not
-  (=
-   (a2
-    (ite 
-     (=> (or (and (= (bvnor (bvnand (bvor (bvand x0 x1) x2) x3) x4) ((_ extract 9 0) v3)) p1) p2) p3)
-     v2
-     6)
-    )
-   (bvudiv (bvudiv v4 v5) (bvudiv (bvudiv v3 v4) (bvudiv v3 v5))))
-  )
- )
-(check-sat)
-(exit)
-- 
2.30.2