diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-15 13:46:31 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-15 18:46:31 +0000 |
| commit | 2ecd897cc1db7153aa63b5caffc0123fc79c8059 (patch) | |
| tree | 421e4829b2505fe0de48ae064c44b8d666f4c67c /test/regress | |
| parent | 6d060743830ab21dc970444688fe1dc2ad34494f (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.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/printer/let_shadowing.smt2 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2 index 14f2316a7..02eb3376a 100644 --- a/test/regress/regress0/printer/let_shadowing.smt2 +++ b/test/regress/regress0/printer/let_shadowing.smt2 @@ -3,7 +3,7 @@ ; SCRUBBER: grep assert ; EXPECT: (assert (let ((_let_1 (* x y))) (and (= _let_1 _let_1) (= _let_1 _let_0)))) ; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((_let_0 Int)) (= 0 _let_0)))))) -; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_2 (and b a))) (and _let_1 _let_2 _let_2 (= 0 _let_0))))))))) +; EXPECT: (assert (let ((_let_1 (and a b))) (and (= _let_1 _let_1) (= _let_1 (forall ((x Int)) (forall ((y Int)) (let ((_let_1 (and b a))) (and (and a b) _let_1 _let_1 (= 0 _let_0))))))))) (set-logic NIA) (declare-const _let_0 Int) (declare-const x Int) |