From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Wed, 11 May 2011 05:17:11 +0000 (+0000)
Subject: Extra test cases that simplify down to nothing.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=3ffd13f8ed538d81cd99f0eda4f8168a612f769b;p=francis%2Fstp.git

Extra test cases that simplify down to nothing.

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

diff --git a/unit_test/alwaysTrue.smt2 b/unit_test/alwaysTrue.smt2
new file mode 100644
index 0000000..4d1eafe
--- /dev/null
+++ b/unit_test/alwaysTrue.smt2
@@ -0,0 +1,13 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(assert (= (or c b) b) )
+(assert (ite (= (or c b) b) c b ))
+
+(exit)
\ No newline at end of file
diff --git a/unit_test/pure2.smt2 b/unit_test/pure2.smt2
new file mode 100644
index 0000000..9f654c8
--- /dev/null
+++ b/unit_test/pure2.smt2
@@ -0,0 +1,39 @@
+
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status sat)
+
+; The below should simplify down to m.
+;  108:(OR 
+;  50:m
+;   52:(AND 
+;     48:l
+;     50:m))
+;(declare-fun l () Bool)
+;(declare-fun m () Bool)
+;(assert (or m (and l m)))
+
+(declare-fun a () Bool)
+(declare-fun b () Bool)
+(declare-fun c () Bool)
+(declare-fun d () Bool)
+(declare-fun e () Bool)
+
+; Simplifies as expected.
+; (assert (or (or a b) (and a b)))
+
+(assert (or (or a b) (or c (and a d))))
+
+
+;(assert (or (or a (and a d)) (or b c)))
+
+
+
+
+
+
+
+(check-sat)
+(exit)
+
diff --git a/unit_test/writing_same.smt2 b/unit_test/writing_same.smt2
new file mode 100644
index 0000000..3fae392
--- /dev/null
+++ b/unit_test/writing_same.smt2
@@ -0,0 +1,13 @@
+(set-info :source | fuzzsmt 0.3 |)
+(set-logic  QF_ABV)
+(set-info :status sat)
+(declare-fun v5572 () (_ BitVec 8))
+(declare-fun v5573 () (_ BitVec 8))
+
+
+(declare-fun v5574 () (_ BitVec 2))
+(declare-fun a5575 () (Array (_ BitVec 8) (_ BitVec 8)))
+
+(assert(= v5572 (select (store a5575 v5572 (select a5575 v5572)) v5573)))
+
+(check-sat)