test/regress/regress0/quantifiers/cond-var-elim-binary.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16

(set-logic BV)
(set-info :status unsat)
(declare-fun k_42 () (_ BitVec 32))
(declare-fun k_332 () (_ BitVec 32))
(declare-fun k_28 () (_ BitVec 32))

(assert (and 
(bvult k_332 k_42)

(forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or 
  (and (not (bvult y (_ bv65539 32))) (not (= (_ bv1 32) x))) 
  (not (bvult k_332 (bvmul x k_42)))) )
)
)

(check-sat)