added more tests

diff --git a/test/regress/regress0/bv/inequality04.smt2 b/test/regress/regress0/bv/inequality04.smt2
new file mode 100644 (file)
index 0000000..7b5dbd7
--- /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 (file)
index 0000000..d8cf9cf
--- /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