projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a223557) | patch
Fix trivial explantions in sequences array solver (#7973)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 21 Jan 2022 00:42:51 +0000 (18:42 -0600)
committerGitHub <noreply@github.com>
Fri, 21 Jan 2022 00:42:51 +0000 (16:42 -0800)
commitcd91ef90ea461cd2d81ea69528c027f53f48b414
treecda062777c87c9f9125350798dc14e6f9fe498eatree
parenta22355748973e5e567e9543a7f036a23d616bbbdcommit | diff
Fix trivial explantions in sequences array solver (#7973)

Also tightens the explanation slightly, we were previously adding a spurious equality to the representative, instead of the base of the normal form.
src/theory/strings/array_solver.cpp diff | blob | history
test/regress/regress0/seq/array/update-word-eq.smt2 diff | blob | history