From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 20 Mar 2013 04:59:15 +0000 (-0400)
Subject: one more ineq regression
X-Git-Tag: cvc5-1.0.0~7361^2~33
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0a319e44fb2630d05207bba40eab290a805eab2b;p=cvc5.git

one more ineq regression
---

diff --git a/test/regress/regress0/bv/inequality03.smt2 b/test/regress/regress0/bv/inequality03.smt2
new file mode 100644
index 000000000..a47551d14
--- /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)