diff options
Diffstat (limited to 'test/regress/regress0')
| -rw-r--r-- | test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 b/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 new file mode 100644 index 000000000..edf780b4e --- /dev/null +++ b/test/regress/regress0/quantifiers/cond-var-elim-binary.smt2 @@ -0,0 +1,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) |