From 0a319e44fb2630d05207bba40eab290a805eab2b Mon Sep 17 00:00:00 2001
From: Liana Hadarean <lianahady@gmail.com>
Date: Wed, 20 Mar 2013 00:59:15 -0400
Subject: [PATCH] one more ineq regression

---
 test/regress/regress0/bv/inequality03.smt2 | 10 ++++++++++
 1 file changed, 10 insertions(+)
 create mode 100644 test/regress/regress0/bv/inequality03.smt2

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)
-- 
2.30.2