one more ineq regression

diff --git a/test/regress/regress0/bv/inequality03.smt2 b/test/regress/regress0/bv/inequality03.smt2
new file mode 100644 (file)
index 0000000..a47551d
--- /dev/null
+++ b/test/regress/regress0/bv/inequality03.smt2
@@ -0,0 +1,10 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 16))
+(assert (and
+        (bvult v0 (_ bv3 16))
+        (bvult (_ bv2 16) v0)))
+(check-sat)
+(exit)