projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 8ff3b30) | patch
Ensure legal elimination for witness rewrite (#4688)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Fri, 10 Jul 2020 01:07:21 +0000 (20:07 -0500)
committerGitHub <noreply@github.com>
Fri, 10 Jul 2020 01:07:21 +0000 (20:07 -0500)
commitba7cda7a9cb02a38b1cf8fd9fbd85304a9056a5e
tree3d7d957f19d6cda9de4022c93c9ea01fad4fe6b8tree
parent8ff3b306b7b35bc1040a6caee759929c4e497373commit | diff
Ensure legal elimination for witness rewrite (#4688)

Fixes #4685.

A recent commit #4661 added assertions for checking whether a witness rewrite corresponded to a legal elimination. #4685 demonstrates that these assertions can be violated and hence should be checked to ensure the rewrite is sound.
src/theory/builtin/theory_builtin_rewriter.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/quantifiers/issue4685-wrewrite.smt2 [new file with mode: 0644] blob