benchmark to show that we don't rewrite bvsmod correctly

the definition in smtlib was buggy and was changed on 2011-06-15
check http://goedel.cs.uiowa.edu/smtlib/logics/QF_BV.smt2

1 files changed, 28 insertions, 0 deletions

diff --git a/test/regress/regress0/bv/bvsmod.smt2 b/test/regress/regress0/bv/bvsmod.smt2
new file mode 100644
index 000000000..384e3c7b8
--- /dev/null
+++ b/test/regress/regress0/bv/bvsmod.smt2
@@ -0,0 +1,28 @@
+(set-logic  QF_BV)
+
+(set-info :status unsat)
+
+(define-fun bvsmod_def ((s (_ BitVec 13)) (t (_ BitVec 13))) (_ BitVec 13)
+     (let ((msb_s ((_ extract 12 12) s))
+           (msb_t ((_ extract 12 12) t)))
+       (let ((abs_s (ite (= msb_s #b0) s (bvneg s)))
+             (abs_t (ite (= msb_t #b0) t (bvneg t))))
+         (let ((u (bvurem abs_s abs_t)))
+           (ite (= u (_ bv0 13))
+                u
+           (ite (and (= msb_s #b0) (= msb_t #b0))
+                u
+           (ite (and (= msb_s #b1) (= msb_t #b0))
+                (bvadd (bvneg u) t)
+           (ite (and (= msb_s #b0) (= msb_t #b1))
+                (bvadd u t)
+                (bvneg u)))))))))
+
+(define-fun a () (_ BitVec 13) (_ bv30 13))
+(define-fun b () (_ BitVec 13) (_ bv8190 13))
+
+(assert (not (= (bvsmod_def a b) (bvsmod a b))))
+
+(check-sat)
+
+(exit)