diff --git a/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 b/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 index 1295ef44fba..e422951b90f 100644 --- a/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 +++ b/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 @@ -2,5 +2,7 @@ ; EXPECT: unsat (set-logic ALL) (declare-fun x () (_ BitVec 4000)) -(assert (< (bv2nat x) 0)) +(declare-fun y () (_ BitVec 4000)) +(assert (< (bv2nat x) (bv2nat y) )) +(assert (= (+ (bv2nat x) (bv2nat y)) 0)) (check-sat)