(ext-rew-prep) refutation unsoundness on string formula #6520
Description
Commit: cd1f1c3
OS: Ubuntu 18.04
It also affects cvc4-1.8, but not cvc4-1.7.
[568] % cvc5 -q small.smt2
sat
[569] % cvc5 -q --ext-rew-prep small.smt2
unsat
[570] % cvc4-1.8 -q --ext-rew-prep small.smt2
unsat
[571] % cvc4-1.7 -q --ext-rew-prep small.smt2
sat
[572] %
[572] % cat small.smt2
(declare-fun a () String)
(declare-fun b () String)
(declare-fun c () String)
(assert (= (str.++ "AB" b c) (str.++ c "B" a)))
(check-sat)
[573] %
Metadata
Metadata
Assignees
Labels
No labels