summaryrefslogtreecommitdiff
path: root/test/regress/regress0
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2020-02-20 14:49:02 -0600
committerGitHub <noreply@github.com>2020-02-20 14:49:02 -0600
commit5489ef01beb91e256e343e2fd2d734b48b42ad6e (patch)
treef6a535c768ae4f3cfbbed765b0697300f4412657 /test/regress/regress0
parent32fdf625f66b8ebf260756962a53d63eec771c12 (diff)
Remove front-end support for Chain (#3767)
Diffstat (limited to 'test/regress/regress0')
-rw-r--r--test/regress/regress0/printer/let_shadowing.smt26
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/printer/let_shadowing.smt2 b/test/regress/regress0/printer/let_shadowing.smt2
index 9b5ffe747..017479871 100644
--- a/test/regress/regress0/printer/let_shadowing.smt2
+++ b/test/regress/regress0/printer/let_shadowing.smt2
@@ -1,9 +1,9 @@
; REQUIRES: dumping
; COMMAND-LINE: --dump raw-benchmark --preprocess-only
; SCRUBBER: grep assert
-; EXPECT: (assert (let ((_let_1 (* x y))) (= _let_1 _let_1 _let_0)))
-; EXPECT: (assert (let ((_let_1 (and a b))) (= _let_1 _let_1 (forall ((_let_0 Int)) (= 0 _let_0) ))))
-; EXPECT: (assert (let ((_let_1 (and a b))) (= _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 (* 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))) ) )))))
(set-logic NIA)
(declare-const _let_0 Int)
(declare-const x Int)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback