From 59e34ed244689b87d781622ec12164e3a96032be Mon Sep 17 00:00:00 2001 From: trevor_hansen Date: Fri, 18 Mar 2011 12:32:07 +0000 Subject: [PATCH] Test case for r1217. git-svn-id: https://stp-fast-prover.svn.sourceforge.net/svnroot/stp-fast-prover/trunk/stp@1218 e59a4935-1847-0410-ae03-e826735625c1 --- unit_test/mult.smt2 | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 unit_test/mult.smt2 diff --git a/unit_test/mult.smt2 b/unit_test/mult.smt2 new file mode 100644 index 0000000..2f52f5d --- /dev/null +++ b/unit_test/mult.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 15)) +(declare-fun z () (_ BitVec 55)) + +(assert (not (= ((_ sign_extend 25) (bvmul ((_ sign_extend 20) x) ((_ sign_extend 15) y))) + (bvmul ((_ sign_extend 45) x) ((_ sign_extend 40) y) ) ) +) +) + +(declare-fun a () (_ BitVec 15)) +(declare-fun b () (_ BitVec 55)) +(assert (= (_ bv44444444444444444 65) (bvadd ((_ sign_extend 50 ) a ) ((_ sign_extend 10 ) b )))) + + +(check-sat) +(exit) + + \ No newline at end of file -- 2.47.3