projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 320c48b) | patch
Use top-level substitutions in ITE simp (#6651)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 1 Jun 2021 18:58:49 +0000 (13:58 -0500)
committerGitHub <noreply@github.com>
Tue, 1 Jun 2021 18:58:49 +0000 (13:58 -0500)
commit7eff8fb5145752b100a9d04c834973e794d9a860
treee12f2704467c6d6629eecb6d56c29e8933e5b908tree
parent320c48b1c82feb7a5d55af39d0cdbb7a1c2c6ff2commit | diff
Use top-level substitutions in ITE simp (#6651)

With this PR, we use the central top-level substitutions instance in the ITE simplification preprocessing pass. Previously the ITE simplification pass maintained its own copy of the substitutions.

Since the top-level substitutions now are the authority on models, this led to model failures after this change: ac8cf53#diff-30677c5a1752b1d0e83ef25fd2cfb8949576ea42cf7821fe0ac00ebbd0122f8aL276.
This PR corrects the issue.

This is required for SMT-COMP.
src/preprocessing/passes/ite_simp.cpp diff | blob | history
src/theory/arith/arith_ite_utils.cpp diff | blob | history
src/theory/arith/arith_ite_utils.h diff | blob | history