diff options
| -rw-r--r-- | test/regress/regress0/unconstrained/Makefile.am | 4 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/bvbool3.smt2 | 3 | ||||
| -rw-r--r-- | test/regress/regress0/unconstrained/bvbool3.smt3 | 37 |
3 files changed, 4 insertions, 40 deletions
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) |