Potential performance issue on QF_BV formula

[rainoftime]

Hi, for the following formula

(set-logic QF_BV)
(declare-fun _substvar_199_ () (_ BitVec 427))
(declare-fun _substvar_238_ () (_ BitVec 427))
(check-sat)
(assert (= (_ bv0 427) (_ bv0 427) (bvudiv _substvar_199_ _substvar_238_)))
(check-sat)

CVC4 nightly https://cvc4.cs.stanford.edu/downloads/builds/x86_64-linux-opt/unstable/cvc4-2020-09-16-x86_64-linux-opt

time ./yices_smt2 --incremental yy.smt2
sat
sat
real    0m1.862s
user    0m1.654s
sys     0m0.208s

time ./stp yy.smt2
sat
sat
real    0m0.009s
user    0m0.003s
sys     0m0.006s


./cvc4 -i --tlimit=60000 yy.smt2                                                                                                                        
CVC4 interrupted by timeout.

[aniemetz]

This is solved immediately when unconstrained simplification is enabled (--unconstrained-simp ). Note: We don't support unconstrained simplification when solving incrementally, I removed the first check-sat call (which is pretty pointless anyways) for this.

[aniemetz]

Bitwuzla stats (without unconstrained simplification):

sat
sat

real    0m2.296s
user    0m2.087s
sys     0m0.207s