[consolidated] hang on small instances (string, bit-vector)

[zhendongsu]

Commit: 0b3bbc2
OS: Ubuntu 22.04

[523] % time z3-4.11.2 small.smt2 
sat

real	0m0.112s
user	0m0.035s
sys	0m0.009s
[524] % timeout -s 9 10 z3release small.smt2 
Killed
[525] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(assert (str.<= a b))
(assert (str.contains b a))
(check-sat)

[zhendongsu]

Another instance:

[704] % time z3-4.11.2 small.smt2 
sat

real	0m0.513s
user	0m0.215s
sys	0m0.011s
[705] % timeout -s 9 30 z3release small.smt2 
Killed
[706] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.<= a (str.replace "A" "" (str.replace b c ""))))
(check-sat)

[zhendongsu]

[669] % time z3-4.11.2 small.smt2 
sat

real	0m0.289s
user	0m0.090s
sys	0m0.011s
[670] % timeout -s 9 30 z3release small.smt2 
Killed
[671] % cat small.smt2 
(declare-const a (_ BitVec 32))
(declare-const b (_ BitVec 32))
(assert (bvult a (bvor (bvurem b a) #x00000000)))
(check-sat)

[zhendongsu]

[653] % time z3-4.11.2 small.smt2 
sat

real	0m0.091s
user	0m0.025s
sys	0m0.017s
[654] % timeout -s 9 30 z3release small.smt2 
Killed
[655] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(assert (str.<= a (str.replace b a b)))
(check-sat)

[zhendongsu]

It appears to reproduce for at least 4.8.17 and later.

[528] % time cvc5 -q small.smt2 
sat

real	0m0.007s
user	0m0.003s
sys	0m0.003s
[529] % timeout -s 9 30 z3release small.smt2 
Killed
[530] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof (str.replace_all (str.replace b a "") "" c) c))
(assert (str.contains c a))
(check-sat)

[zhendongsu]

[541] % time z3-4.8.17 small.smt2 
sat

real	0m0.650s
user	0m0.630s
sys	0m0.020s
[542] % timeout -s 9 30 z3release small.smt2 
Killed
[543] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof (str.replace a b "") a))
(assert (str.contains a c))
(check-sat)

[zhendongsu]

[574] % time z3-4.8.5 small.smt2 
sat

real	0m0.020s
user	0m0.013s
sys	0m0.004s
[575] % timeout -s 9 60 z3release small.smt2 
Killed
[576] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(declare-const c String)
(assert (str.prefixof (str.replace a c "") b))
(assert (str.suffixof a b))
(check-sat)

[zhendongsu]

[589] % time z3-4.11.2 small.smt2 
sat

real	0m0.491s
user	0m0.403s
sys	0m0.088s
[590] % timeout -s 9 60 z3release small.smt2 
Killed
[591] % cat small.smt2 
(declare-const a (_ BitVec 64))
(declare-const b (_ BitVec 64))
(assert (bvult a (bvurem b a)))
(check-sat)

[zhendongsu]

[613] % time z3-4.11.2 small.smt2 
sat

real	0m0.035s
user	0m0.017s
sys	0m0.017s
[614] % timeout -s 9 60 z3release small.smt2 
Killed
[615] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(assert (or (str.<= a b) (str.contains b a)))
(check-sat)

[zhendongsu]

[567] % time z3-4.11.2 small.smt2 
sat

real	0m0.036s
user	0m0.020s
sys	0m0.016s
[568] % timeout -s 9 60 z3release small.smt2 
Killed
[569] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(assert (not (str.prefixof (str.replace a b "") b)))
(check-sat)

[zhendongsu]

[551] % time z3-4.11.0 small.smt2 
sat

real    0m0.040s
user    0m0.010s
sys     0m0.017s
[552] % timeout -s 9 60 z3-4.11.2 small.smt2 
Killed
[553] % timeout -s 9 60 z3release small.smt2 
Killed
[554] % cat small.smt2 
(declare-const a String)
(declare-const b String)
(assert (str.contains (str.replace a b a) a))
(check-sat)