projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 14944f1) | patch
Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 30 Jun 2021 12:52:35 +0000 (07:52 -0500)
committerGitHub <noreply@github.com>
Wed, 30 Jun 2021 12:52:35 +0000 (09:52 -0300)
commita633cd03e1fe118a0e5a7b50db25395b387173a1
tree4e2aec1a30a0fc5bc90b6731bf0b56d9ed8b181dtree
parent14944f1115fa2ad20afa3873626c2804731aff71commit | diff
Fix pre vs. post-rewrite in proofs for theory preprocessor (#6801)

This changes an annotation of a step of rewriting from "post" to "pre" in the theory preprocessor.
Fixes #6754.
src/proof/conv_proof_generator.cpp diff | blob | history
src/theory/theory_preprocessor.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/preprocess/issue6754-tpp.smt2 [new file with mode: 0644] blob