projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 1415f62) | patch
Fix tracker in SubstitutionMap (#7829)
authorGereon Kremer <gkremer@stanford.edu>
Fri, 17 Dec 2021 20:48:38 +0000 (12:48 -0800)
committerGitHub <noreply@github.com>
Fri, 17 Dec 2021 20:48:38 +0000 (20:48 +0000)
commitccc50ccd4b5021c5c83f350954ac1df27160184f
tree789965c60c306acc0394200a791b1ad73dc702e5tree
parent1415f6234cf8ca17711d384863a4a21867477577commit | diff
Fix tracker in SubstitutionMap (#7829)

This PR fixes a subtle issue in #7787 where the rhs (instead of the lhs) of the applied substitution was inserted into the tracker.
Fixes cvc5/cvc5-projects#388
src/theory/substitutions.cpp diff | blob | history
test/unit/api/cpp/CMakeLists.txt diff | blob | history
test/unit/api/cpp/theory_arith_nl_black.cpp [new file with mode: 0644] blob