Fixed broken test case, removed one that is a mistake

diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am
index 984cd4d459e92935efe4b12493088fd26763dc0e..d3adc2167fcbadbce604bbc1f3aca4e1decbda41 100644 (file)
--- 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 6f72246f06748b68dd4815fde729be3c0186119c..a689804f767e5c7e9f845bba8d44c6d61b22eda9 100644 (file)
--- 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 (file)
index 7c93626..0000000
--- 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)