diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-13 02:28:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-06-13 02:28:46 +0000 |
commit | 134c6dc95199bc57013d07e0992f89254f49038b (patch) | |
tree | 85a499d310d222f1d6d84c8e35ba3be62b9cc78d /test/regress/regress0/bv | |
parent | 37a8af9ca9242be9417dd5cea15dd641d18f4b84 (diff) |
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
Diffstat (limited to 'test/regress/regress0/bv')
-rw-r--r-- | test/regress/regress0/bv/bvsmod.smt2 | 28 |
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) |