From f96ecf4996402e619366ae1aa9a3d9df0c61ce2f Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Tue, 10 Apr 2012 05:07:03 +0000 Subject: [PATCH] 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 --- unit_test/propagate.smt2 | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) create mode 100644 unit_test/propagate.smt2 diff --git a/unit_test/propagate.smt2 b/unit_test/propagate.smt2 new file mode 100644 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) + -- 2.47.3