search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
325 stars 63 forks source link

Potential performance issue on QF_ABV formulas #144

Open rainoftime opened 3 years ago

rainoftime commented 3 years ago

Hi, for the following formula 

(set-logic QF_ABV)
(declare-const bv_40-0 (_ BitVec 40))
(assert (bvugt (bvurem ((_ rotate_right 6) bv_40-0) bv_40-0) bv_40-0))
(check-sat)

boolector 6fce0ac35ec

time ./yices_smt2 yy.smt2
unsat
real    0m0.258s
user    0m0.253s
sys     0m0.005s

/boolector --time=10 yy.smt2
[btor>main] ALARM TRIGGERED: time limit 10 seconds reached
unknown
rainoftime commented 3 years ago

Another formula

(set-logic QF_ABV)
(declare-fun _substvar_26_ () (_ BitVec 410))
(declare-fun _substvar_30_ () (Array (_ BitVec 10) (_ BitVec 410)))
(declare-fun _substvar_32_ () (Array (_ BitVec 10) (_ BitVec 410)))
(declare-fun _substvar_34_ () (Array (_ BitVec 10) (_ BitVec 410)))
(declare-fun _substvar_52_ () (_ BitVec 410))
(declare-const arr-5514152941987887040_5514152942420897040-0 (Array (_ BitVec 10) (_ BitVec 410)))
(assert (= _substvar_34_ arr-5514152941987887040_5514152942420897040-0 _substvar_32_ _substvar_30_ (store arr-5514152941987887040_5514152942420897040-0 (_ bv0 10) (bvmul _substvar_26_ _substvar_52_))))
(check-sat)
time ./yices_smt2 yy.smt2
sat

real    0m0.003s
user    0m0.000s
sys     0m0.003s

time /.boolector  yy.smt2
sat

real    0m10.077s
user    0m9.524s
sys     0m0.552s