Commit: 0133367
OS: Ubuntu 18.04
Note: (1) might be related to #6636, but cvc4-1.8 produces a fatal failure on the other instance for #6636; (2) model validation detects the produced invalid model
[519] % cvc4-1.8 -q --strings-exp small.smt2
unsat
[520] % cvc5 -q --strings-exp small.smt2
sat
[521] %
[521] % cat small.smt2
(declare-fun a () String)
(assert (= (str.len a) 2))
(assert (= (str.len (str.replace_re_all a (str.to_re "A") "B")) 3))
(check-sat)
[522] %
Commit: 0133367
OS: Ubuntu 18.04
Note: (1) might be related to #6636, but cvc4-1.8 produces a fatal failure on the other instance for #6636; (2) model validation detects the produced invalid model