]> git.unchartedbackwaters.co.uk Git - francis/stp.git/commitdiff
oops. Meant to add this too.
authortrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 11 Apr 2011 15:11:08 +0000 (15:11 +0000)
committertrevor_hansen <trevor_hansen@e59a4935-1847-0410-ae03-e826735625c1>
Mon, 11 Apr 2011 15:11:08 +0000 (15:11 +0000)
git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1266 e59a4935-1847-0410-ae03-e826735625c1

unit_test/bvnot.smt2 [new file with mode: 0644]

diff --git a/unit_test/bvnot.smt2 b/unit_test/bvnot.smt2
new file mode 100644 (file)
index 0000000..fdd2066
--- /dev/null
@@ -0,0 +1,20 @@
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "check")
+(set-info :status unsat)
+(declare-fun x () (_ BitVec 6))
+
+
+
+; This is always true. 
+(assert 
+        (=
+               (bvnot x  )
+               x
+       )
+)
+
+
+(check-sat)
+(exit)
+