Significant slowdown from 4.8.5 to 4.8.6 #4178
Description
Here are timings for the attached prob.txt using z3 4.8.5 and 4.8.6. Note the slowdown: less than 1 second to almost 7 minutes.
$ time z3 prob.txt
sat
(:version "4.8.5")
real 0m0.630s
user 0m0.622s
sys 0m0.008s
$ time z3 prob.txt
sat
(:version "4.8.6")
real 6m50.631s
user 6m50.536s
sys 0m0.037s
These experiments were performed on an Ubuntu 18.04.4 machine. z3 was installed using the PyPi package.
prob.txt is pasted here for convenience:
(declare-fun SVALUE_3 () (_ BitVec 256))
(declare-fun SVALUE_1 () (_ BitVec 256))
(declare-fun BV () (_ BitVec 256))
(declare-fun a_414 () (_ BitVec 256))(assert (= a_414 #x0000000000000000000000000000000000000000000000008ac7230489e80000))
(declare-fun a_415 () (_ BitVec 256))(assert (= a_415 (bvneg SVALUE_1)))
(declare-fun a_416 () (_ BitVec 256))(assert (= a_416 (bvadd a_414 a_415)))
(declare-fun a_417 () Bool)(assert (= a_417 (bvuge a_416 SVALUE_3)))
(declare-fun a_418 () (_ BitVec 256))(assert (= a_418 (bvadd SVALUE_1 SVALUE_3)))
(declare-fun a_419 () (_ BitVec 256))(assert (= a_419 #x0000000000000000000000000000000000000000000000000000000000000000))
(declare-fun a_420 () Bool)(assert (= a_420 (bvugt a_418 a_419)))
(declare-fun a_421 () Bool)(assert (= a_421 (not a_420)))
(declare-fun a_422 () (_ BitVec 256))(assert (= a_422 #x000000000000000000000000000000000000000000000000000000000000015a))
(declare-fun a_423 () (_ BitVec 256))(assert (= a_423 #x00000000000000000000000000000000000000000000000000000000000000bf))
(declare-fun a_424 () (_ BitVec 256))(assert (= a_424 (ite a_421 a_422 a_423)))
(declare-fun a_425 () (_ BitVec 256))(assert (= a_425 #x00000000000000000000000000000000000000000000000000000000000003e8))
(declare-fun a_426 () (_ BitVec 256))(assert (= a_426 (bvadd SVALUE_1 SVALUE_3)))
(declare-fun a_427 () (_ BitVec 256))(assert (= a_427 #x00000000000000000000000000000000000000000000000000000000000003e8))
(declare-fun a_428 () (_ BitVec 256))(assert (= a_428 #x0000000000000000000000000000000000000000000000008ac7230489e80000))
(declare-fun a_429 () Bool)(assert (= a_429 (bvule SVALUE_1 a_428)))
(assert (= a_429 true))
(assert (bvult a_426 a_427))
(assert (bvult SVALUE_1 a_425))
(assert (= BV a_424))
(assert (= a_417 true))
(check-sat)
(get-info :version)