projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: e2ec4e5) | patch
Do not track processed in remove term formulas loop (#5791)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Wed, 20 Jan 2021 15:56:02 +0000 (09:56 -0600)
committerGitHub <noreply@github.com>
Wed, 20 Jan 2021 15:56:02 +0000 (09:56 -0600)
commit6235612ddfdd59432eedf771a65c248d5b3d0469
treedd148ce679835f32e6f736e5269130db27ff4f41tree
parente2ec4e5401eba4ef63539ddb7c1f3a54301de4b1commit | diff
Do not track processed in remove term formulas loop (#5791)

The assertion/tracking was spurious, since an eliminated term may occur in multiple contexts.

Fixes #5728 (which I could not reproduce currently). Adds a regression from a duplicate of that issue.
src/smt/term_formula_removal.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress1/issue5739-rtf-processed.smt2 [new file with mode: 0644] blob