Testcase to check it realises neg and not are both inverse-able.

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

diff --git a/unit_test/propagate.smt2 b/unit_test/propagate.smt2
new file mode 100644 (file)
index 0000000..c42e4ed
--- /dev/null
+++ b/unit_test/propagate.smt2
@@ -0,0 +1,24 @@
+
+(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 () (_ BitVec 20))
+
+; Needs to realise that you can take the inverse of bvneg, or bvnot.
+(assert (= (bvnot v0) (bvneg v1) ))
+(assert (not (= v0 v1)))
+
+
+(declare-fun v2 () (_ BitVec 20))
+(declare-fun v3 () (_ BitVec  20))
+(assert (= (bvmul (_ bv05 20 ) (bvnot v2)) (bvashr v3 v3) ))
+;(assert (= v2 v3))
+
+
+
+(check-sat)
+(exit)
+