From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 23 Feb 2011 07:09:20 +0000 (+0000)
Subject: Extra test cases that should be simplified down to nothing.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=d5845caa1f17afdf47600684488a6a8a4ce14b68;p=francis%2Fstp.git

Extra test cases that should be simplified down to nothing.

git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1160 e59a4935-1847-0410-ae03-e826735625c1
---

diff --git a/unit_test/harald.smt2 b/unit_test/harald.smt2
new file mode 100644
index 0000000..dfc48dc
--- /dev/null
+++ b/unit_test/harald.smt2
@@ -0,0 +1,20 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun x () (_ BitVec 15))
+(declare-fun y () (_ BitVec 15))
+(declare-fun z () (_ BitVec 15))
+
+
+
+(assert (= y (bvadd x (_ bv1 15))))
+(assert (= z (bvadd y (_ bv1 15))))
+
+(assert (= (bvmul y y )  (bvadd (_ bv1 15) (bvmul x z))))
+
+
+
+(check-sat)
+(exit)
+
diff --git a/unit_test/mod.smt2 b/unit_test/mod.smt2
new file mode 100644
index 0000000..0901292
--- /dev/null
+++ b/unit_test/mod.smt2
@@ -0,0 +1,25 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun x () (_ BitVec 15))
+(declare-fun y () (_ BitVec 15))
+
+
+
+; This is always true. 
+(assert 
+	(bvuge
+		(_ bv9 15)
+		(bvurem (bvand x y) (_ bv10 15))
+	)
+)
+
+; So unconstrained variables don't eliminate immediately.
+(assert (not (= x y)))
+
+
+
+(check-sat)
+(exit)
+
diff --git a/unit_test/pure.smt2 b/unit_test/pure.smt2
new file mode 100644
index 0000000..69918a2
--- /dev/null
+++ b/unit_test/pure.smt2
@@ -0,0 +1,18 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+(declare-fun v0 () (_ BitVec 20))
+(declare-fun v1 () Bool)
+
+
+(assert (or v1 (= (bvsmod v0 (bvnot v0)) (_ bv23211 20) )))
+
+
+
+
+(check-sat)
+(exit)
+
+