diff options
Diffstat (limited to 'test/regress/regress0/bv/unsound1.smt2')
| -rw-r--r-- | test/regress/regress0/bv/unsound1.smt2 | 23 |
1 files changed, 0 insertions, 23 deletions
diff --git a/test/regress/regress0/bv/unsound1.smt2 b/test/regress/regress0/bv/unsound1.smt2 deleted file mode 100644 index 60e764537..000000000 --- a/test/regress/regress0/bv/unsound1.smt2 +++ /dev/null @@ -1,23 +0,0 @@ -(set-logic QF_BV) -(set-info :status sat) -(declare-fun v0 () (_ BitVec 4)) -(assert (let ((e1(_ bv0 1))) -(let ((e2(_ bv11134 16))) -(let ((e3 (bvadd e2 ((_ sign_extend 12) v0)))) -(let ((e4 (ite (= e2 ((_ sign_extend 12) v0)) (_ bv1 1) (_ bv0 1)))) -(let ((e5 (bvlshr e3 ((_ sign_extend 12) v0)))) -(let ((e6 (bvxnor e2 ((_ zero_extend 12) v0)))) -(let ((e7 (ite (bvult ((_ sign_extend 15) e1) e2) (_ bv1 1) (_ bv0 1)))) -(let ((e8 (bvugt e7 e1))) -(let ((e9 (bvule ((_ sign_extend 3) e7) v0))) -(let ((e10 (bvsgt e5 ((_ zero_extend 12) v0)))) -(let ((e11 (= e6 e3))) -(let ((e12 (bvslt ((_ zero_extend 15) e4) e5))) -(let ((e13 (bvugt e5 e2))) -(let ((e14 (ite e10 e8 e10))) -(let ((e15 (xor e13 e11))) -(let ((e16 (xor e14 e15))) -(let ((e17 (ite e9 e12 e16))) -e17 -)))))))))))))))))) -(check-sat) |