From 6b01e8740111e69219e5d733e1123955f8cd2ea7 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 5 Jun 2019 13:01:34 -0700 Subject: Prevent letification from shadowing variables (#3042) Fixes #3005. When printing nodes, we introduce `let` expressions on the fly. However, when doing that, we have to be careful that we don't shadow existing variables with the same name. When quantifiers are involved, we do not descend into the quantifiers to avoid letifying terms with bound variables that then go out of scope (see #1863). Thus, to avoid shadowing variables appearing in quantifiers, we have to collect all the variables appearing in that term to make sure that the let does not shadow them. In #3005, the issue was caused by a `let` that was introduced outside of a quantifier and then was shadowed in the body of the quantifier by another `let` introduced for that body. --- test/regress/CMakeLists.txt | 1 + 1 file changed, 1 insertion(+) (limited to 'test/regress/CMakeLists.txt') diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index b63930569..0a5f0a972 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -586,6 +586,7 @@ set(regress_0_tests regress0/printer/bv_consts_bin.smt2 regress0/printer/bv_consts_dec.smt2 regress0/printer/empty_symbol_name.smt2 + regress0/printer/let_shadowing.smt2 regress0/printer/tuples_and_records.cvc regress0/push-pop/boolean/fuzz_12.smt2 regress0/push-pop/boolean/fuzz_13.smt2 -- cgit v1.2.3