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

diff --git a/unit_test/mult.smt2 b/unit_test/mult.smt2
new file mode 100644 (file)
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