better test

yoni206 · Jun 6, 2024 · c8e445b · c8e445b
1 parent 442cf96
commit c8e445b
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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)