From: trevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Date: Sat, 14 Jan 2012 02:16:46 +0000 (+0000)
Subject: Extra unit test.
X-Git-Url: https://git.unchartedbackwaters.co.uk/w/?a=commitdiff_plain;h=9509ee8fef8beb727b9814773cf9412db4e4c11c;p=francis%2Fstp.git

Extra unit test.

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

diff --git a/unit_test/bvge3.smt2 b/unit_test/bvge3.smt2
new file mode 100644
index 0000000..3b3425b
--- /dev/null
+++ b/unit_test/bvge3.smt2
@@ -0,0 +1,22 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 10))
+(declare-fun y () (_ BitVec 10))
+
+
+; 
+(assert 
+	 (bvslt
+		(bvlshr (concat (_ bv0 10)  y )  (_ bv2 20) )
+		(concat (_ bv64 10)  x )
+	)
+)
+
+(assert (not (= x y)))
+
+
+(check-sat)
+(exit)
+