diff options
Diffstat (limited to 'test/regress/regress0/unconstrained/bvbool3.smt3')
-rw-r--r-- | test/regress/regress0/unconstrained/bvbool3.smt3 | 37 |
1 files changed, 0 insertions, 37 deletions
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) |