diff options
Diffstat (limited to 'test/regress/regress1/bv/divtest.smt2')
| -rw-r--r-- | test/regress/regress1/bv/divtest.smt2 | 53 |
1 files changed, 53 insertions, 0 deletions
diff --git a/test/regress/regress1/bv/divtest.smt2 b/test/regress/regress1/bv/divtest.smt2 new file mode 100644 index 000000000..fe91cb87b --- /dev/null +++ b/test/regress/regress1/bv/divtest.smt2 @@ -0,0 +1,53 @@ +(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) |