[consolidated] hang on small instances (string, bit-vector)
Author: zhendongsuCreated Mar 14, 2024Updated Jul 14, 2026
Commit: https://github.com/Z3Prover/z3/commit/0b3bbc297248849cb17c29e0fbaa23f61bb45716 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)Source: Z3Prover/z3