diff --git a/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 b/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 new file mode 100644 index 00000000000..e22a1ac5edd --- /dev/null +++ b/test/regress/cli/regress0/bv2nat_lemma_ranges_1.smt2 @@ -0,0 +1,6 @@ +; COMMAND: --model-based-arith-bv-conv +; EXPECT: unsat +(set-logic ALL) +(declare-fun x () (_ BitVec 4)) +(assert (< (bv2nat x) 0)) +(check-sat)