projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 02b88b7) | patch
Use fresh variables when miniscoping (#4296)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Tue, 19 May 2020 20:38:05 +0000 (15:38 -0500)
committerGitHub <noreply@github.com>
Tue, 19 May 2020 20:38:05 +0000 (15:38 -0500)
commit6bb98062a5578d126db6a3e8cdca083881893b32
tree6252c581945f90b786864eacc83344a0ed1ebfd0tree
parent02b88b7665df5a6b1a2bce231d7567efdcc4b20acommit | diff
Use fresh variables when miniscoping (#4296)

Fixes #4288.

When applying miniscoping, we previously were reusing variables across quantified formulas in the resulting conjunction. This ensures our miniscoping ensures fresh variables.
src/theory/quantifiers/quantifiers_rewriter.cpp diff | blob | history