projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6d06074) | patch
Letify quantifier bodies independently (#6112)
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>
Mon, 15 Mar 2021 18:46:31 +0000 (13:46 -0500)
committerGitHub <noreply@github.com>
Mon, 15 Mar 2021 18:46:31 +0000 (18:46 +0000)
commit2ecd897cc1db7153aa63b5caffc0123fc79c8059
tree421e4829b2505fe0de48ae064c44b8d666f4c67ctree
parent6d060743830ab21dc970444688fe1dc2ad34494fcommit | diff
Letify quantifier bodies independently (#6112)

This fixes a subtle bug with how quantifier bodies are letified.

It makes our letification more conservative so that let symbols are never pushed inside quantifier bodies, instead quantifier bodies are letified independently of the context.
src/printer/let_binding.cpp diff | blob | history
src/printer/let_binding.h diff | blob | history
src/printer/smt2/smt2_printer.cpp diff | blob | history
test/regress/regress0/printer/let_shadowing.smt2 diff | blob | history