diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2')
-rw-r--r-- | test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2 | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2 b/test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2 deleted file mode 100644 index 38a4ed127..000000000 --- a/test/regress/regress0/quantifiers/intersection-example-onelane.proof-node22337.smt2 +++ /dev/null @@ -1,20 +0,0 @@ -; COMMAND-LINE: --cbqi-bv -; EXPECT: sat -(set-logic BV) -(set-info :status sat) -(declare-fun xI () (_ BitVec 32)) -(declare-fun A () (_ BitVec 32)) -(declare-fun B () (_ BitVec 32)) -(declare-fun vuscore2dollarskuscore80 () (_ BitVec 32)) -(declare-fun I1 () (_ BitVec 32)) -(declare-fun xuscore2dollarskuscore74 () (_ BitVec 32)) -(declare-fun v () (_ BitVec 32)) -(declare-fun ts49uscore0 () (_ BitVec 32)) -(declare-fun V () (_ BitVec 32)) -(declare-fun t87uscore0dollarskuscore0 () (_ BitVec 32)) -(declare-fun ep () (_ BitVec 32)) -(declare-fun I1uscore2dollarskuscore74 () (_ BitVec 32)) -(declare-fun x () (_ BitVec 32)) -(assert (not (exists ((ts49uscore0 (_ BitVec 32))) (let ((?v_0 (bvsge vuscore2dollarskuscore80 (_ bv0 32))) (?v_1 (bvsle vuscore2dollarskuscore80 V)) (?v_3 (bvsdiv (bvmul vuscore2dollarskuscore80 vuscore2dollarskuscore80) (bvmul (_ bv2 32) B))) (?v_2 (bvmul (bvsdiv (_ bv1 32) (_ bv2 32)) (bvadd (bvmul (bvmul (_ bv2 32) t87uscore0dollarskuscore0) vuscore2dollarskuscore80) (bvmul (_ bv2 32) xuscore2dollarskuscore74))))) (=> (and (and (and (and (and (and (and (and (and (and (and (and (and (and (= I1uscore2dollarskuscore74 (_ bv2 32)) (=> (and (bvsle (_ bv0 32) ts49uscore0) (bvsle ts49uscore0 t87uscore0dollarskuscore0)) (and (and ?v_0 ?v_1) (bvsle ts49uscore0 ep)))) (bvsge t87uscore0dollarskuscore0 (_ bv0 32))) (= vuscore2dollarskuscore80 (_ bv0 32))) ?v_0) ?v_1) (bvsgt xI (bvadd xuscore2dollarskuscore74 ?v_3))) (= I1 (_ bv2 32))) (bvslt xI x)) (bvsgt B (_ bv0 32))) (bvsge v (_ bv0 32))) (bvsle v V)) (bvsge A (_ bv0 32))) (bvsgt V (_ bv0 32))) (bvsgt ep (_ bv0 32))) (or (or (= xI xuscore2dollarskuscore74) (bvslt xI ?v_2)) (bvsgt xI (bvadd ?v_2 ?v_3)))))))) -(check-sat) -(exit) |