From: lianah <lianahady@gmail.com>
Date: Thu, 21 Mar 2013 02:33:39 +0000 (-0400)
Subject: added more tests
X-Git-Tag: cvc5-1.0.0~7361^2~31
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6aa211751e7dc697035cf110c253cc36ace69066;p=cvc5.git

added more tests
---

diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2
new file mode 100644
index 000000000..7b5dbd7d5
--- /dev/null
+++ b/test/regress/regress0/bv/inequality04.smt2
@@ -0,0 +1,19 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status unsat)
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvule v0 v1)
+	 (bvule v1 v2)
+	 (bvule v2 v0)
+	 (bvule (_ bv4 16) v0)
+	 (bvult v2 (_ bv5 16))
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/inequality05.smt2 b/test/regress/regress0/bv/inequality05.smt2
new file mode 100644
index 000000000..d8cf9cf99
--- /dev/null
+++ b/test/regress/regress0/bv/inequality05.smt2
@@ -0,0 +1,28 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(declare-fun v6 () (_ BitVec 16))
+(declare-fun v7 () (_ BitVec 16))
+(declare-fun v8 () (_ BitVec 16))
+(declare-fun v9 () (_ BitVec 16))
+(assert (and 
+(bvult v6 v5)
+(bvule v7 v8)
+(bvugt v7 v1)
+(bvuge v4 v1)
+(bvuge v8 v0)
+(bvugt v1 v0)
+(bvuge v1 (_ bv60094 16))
+(bvule v3 v0)
+(bvuge (_ bv47327 16) v6)
+(bvugt v3 v6)
+))
+(check-sat)
+(exit)
\ No newline at end of file