diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-06-05 13:01:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-05 13:01:34 -0700 |
commit | 6b01e8740111e69219e5d733e1123955f8cd2ea7 (patch) | |
tree | 78dfded555702242e0f44aa98924ecce541b7599 /test/regress/CMakeLists.txt | |
parent | 9af5e9653582a18b1871dfc3774ab50dd24463ce (diff) |
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.
Diffstat (limited to 'test/regress/CMakeLists.txt')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 |
1 files changed, 1 insertions, 0 deletions
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 |