diff options
Diffstat (limited to 'test/regress/regress0/bv/divtest.smt2')
-rw-r--r-- | test/regress/regress0/bv/divtest.smt2 | 53 |
1 files changed, 0 insertions, 53 deletions
diff --git a/test/regress/regress0/bv/divtest.smt2 b/test/regress/regress0/bv/divtest.smt2 deleted file mode 100644 index fe91cb87b..000000000 --- a/test/regress/regress0/bv/divtest.smt2 +++ /dev/null @@ -1,53 +0,0 @@ -(set-logic QF_BV) -(set-info :status unsat) -(declare-fun x1 () (_ BitVec 12)) -(declare-fun x2 () (_ BitVec 12)) -(declare-fun x3 () (_ BitVec 12)) - -(declare-fun y1 () (_ BitVec 12)) -(declare-fun y2 () (_ BitVec 12)) -(declare-fun y3 () (_ BitVec 12)) - -(declare-fun z1 () (_ BitVec 12)) -(declare-fun z2 () (_ BitVec 12)) -(declare-fun z3 () (_ BitVec 12)) - -(declare-fun a () (_ BitVec 12)) - -(declare-fun x01 () (_ BitVec 10)) -(declare-fun x02 () (_ BitVec 10)) -(declare-fun x03 () (_ BitVec 10)) - -(declare-fun y01 () (_ BitVec 10)) -(declare-fun y02 () (_ BitVec 10)) -(declare-fun y03 () (_ BitVec 10)) - -(declare-fun z01 () (_ BitVec 10)) -(declare-fun z02 () (_ BitVec 10)) -(declare-fun z03 () (_ BitVec 10)) - -(declare-fun a0 () (_ BitVec 10)) - -(assert -(or -(and - (= a (_ bv0 12)) - (or (not (= (bvudiv x1 a) (bvudiv x2 a))) - (not (= (bvudiv x1 a) (bvudiv x3 a))) - (not (= (bvudiv x2 a) (bvudiv x3 a)))) - (or (and (= x1 y1) (= y1 x2)) - (and (= x1 z1) (= z1 x2))) - (or (and (= x2 y2) (= y2 x3)) - (and (= x2 z2) (= z2 x3)))) - -(and - (= a0 (_ bv0 10)) - (or (not (= (bvurem x01 a0) (bvurem x02 a0))) - (not (= (bvurem x01 a0) (bvurem x03 a0))) - (not (= (bvurem x02 a0) (bvurem x03 a0)))) - (or (and (= x01 y01) (= y01 x02)) - (and (= x01 z01) (= z01 x02))) - (or (and (= x02 y02) (= y02 x03)) - (and (= x02 z02) (= z02 x03)))))) - -(check-sat) |