From dcda37363a4982b5e6cbf1dacba8dee38f588f1e Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Fri, 29 Nov 2024 19:36:59 -0800 Subject: [PATCH] Update golds to match the new higher-order output syntax --- SBVTestSuite/GoldFiles/lambda27.gold | 50 ++++++++++++----------- SBVTestSuite/GoldFiles/lambda28.gold | 50 ++++++++++++----------- SBVTestSuite/GoldFiles/lambda29.gold | 50 ++++++++++++----------- SBVTestSuite/GoldFiles/lambda30.gold | 50 ++++++++++++----------- SBVTestSuite/GoldFiles/lambda31.gold | 60 ++++++++++++++-------------- SBVTestSuite/GoldFiles/lambda32.gold | 60 ++++++++++++++-------------- 6 files changed, 170 insertions(+), 150 deletions(-) diff --git a/SBVTestSuite/GoldFiles/lambda27.gold b/SBVTestSuite/GoldFiles/lambda27.gold index c79a5edf4..4dda75a0c 100644 --- a/SBVTestSuite/GoldFiles/lambda27.gold +++ b/SBVTestSuite/GoldFiles/lambda27.gold @@ -8,7 +8,7 @@ [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] (set-logic ALL) ; has lambda expressions, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -20,31 +20,35 @@ [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- SBV Function definitions +[GOOD] (define-fun-rec |sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool + (ite (= lst (as seq.empty (Seq Int))) + true + (and (select (lambda ((l1_s0 Int)) + (let ((l1_s1 2)) + (let ((l1_s3 0)) + (let ((l1_s7 1)) + (let ((l1_s13 (- 1))) + (let ((l1_s2 (mod l1_s0 l1_s1))) + (let ((l1_s4 (>= l1_s0 l1_s3))) + (let ((l1_s5 (= l1_s2 l1_s3))) + (let ((l1_s6 (or l1_s4 l1_s5))) + (let ((l1_s8 (ite l1_s6 l1_s3 l1_s7))) + (let ((l1_s9 (* l1_s1 l1_s8))) + (let ((l1_s10 (- l1_s2 l1_s9))) + (let ((l1_s11 (> l1_s10 l1_s3))) + (let ((l1_s12 (< l1_s10 l1_s3))) + (let ((l1_s14 (ite l1_s12 l1_s13 l1_s10))) + (let ((l1_s15 (ite l1_s11 l1_s7 l1_s14))) + (let ((l1_s16 (= l1_s13 l1_s15))) + (let ((l1_s17 (+ l1_s1 l1_s10))) + (let ((l1_s18 (ite l1_s16 l1_s17 l1_s10))) + (let ((l1_s19 (= l1_s3 l1_s18))) + l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))))) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) -[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int)) - (let ((l1_s2 2)) - (let ((l1_s4 0)) - (let ((l1_s8 1)) - (let ((l1_s14 (- 1))) - (let ((l1_s3 (mod l1_s1 l1_s2))) - (let ((l1_s5 (>= l1_s1 l1_s4))) - (let ((l1_s6 (= l1_s3 l1_s4))) - (let ((l1_s7 (or l1_s5 l1_s6))) - (let ((l1_s9 (ite l1_s7 l1_s4 l1_s8))) - (let ((l1_s10 (* l1_s2 l1_s9))) - (let ((l1_s11 (- l1_s3 l1_s10))) - (let ((l1_s12 (> l1_s11 l1_s4))) - (let ((l1_s13 (< l1_s11 l1_s4))) - (let ((l1_s15 (ite l1_s13 l1_s14 l1_s11))) - (let ((l1_s16 (ite l1_s12 l1_s8 l1_s15))) - (let ((l1_s17 (= l1_s14 l1_s16))) - (let ((l1_s18 (+ l1_s2 l1_s11))) - (let ((l1_s19 (ite l1_s17 l1_s18 l1_s11))) - (let ((l1_s20 (= l1_s4 l1_s19))) - (let ((l1_s21 (and l1_s0 l1_s20))) - l1_s21))))))))))))))))))))) true s0)) +[GOOD] (define-fun s4 () Bool (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0)) [GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- diff --git a/SBVTestSuite/GoldFiles/lambda28.gold b/SBVTestSuite/GoldFiles/lambda28.gold index 76bdfe595..590e8c325 100644 --- a/SBVTestSuite/GoldFiles/lambda28.gold +++ b/SBVTestSuite/GoldFiles/lambda28.gold @@ -8,7 +8,7 @@ [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] (set-logic ALL) ; has lambda expressions, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -20,31 +20,35 @@ [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- SBV Function definitions +[GOOD] (define-fun-rec |sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool + (ite (= lst (as seq.empty (Seq Int))) + true + (and (select (lambda ((l1_s0 Int)) + (let ((l1_s1 2)) + (let ((l1_s3 0)) + (let ((l1_s7 1)) + (let ((l1_s13 (- 1))) + (let ((l1_s2 (mod l1_s0 l1_s1))) + (let ((l1_s4 (>= l1_s0 l1_s3))) + (let ((l1_s5 (= l1_s2 l1_s3))) + (let ((l1_s6 (or l1_s4 l1_s5))) + (let ((l1_s8 (ite l1_s6 l1_s3 l1_s7))) + (let ((l1_s9 (* l1_s1 l1_s8))) + (let ((l1_s10 (- l1_s2 l1_s9))) + (let ((l1_s11 (> l1_s10 l1_s3))) + (let ((l1_s12 (< l1_s10 l1_s3))) + (let ((l1_s14 (ite l1_s12 l1_s13 l1_s10))) + (let ((l1_s15 (ite l1_s11 l1_s7 l1_s14))) + (let ((l1_s16 (= l1_s13 l1_s15))) + (let ((l1_s17 (+ l1_s1 l1_s10))) + (let ((l1_s18 (ite l1_s16 l1_s17 l1_s10))) + (let ((l1_s19 (= l1_s3 l1_s18))) + l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))))) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) -[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int)) - (let ((l1_s2 2)) - (let ((l1_s4 0)) - (let ((l1_s8 1)) - (let ((l1_s14 (- 1))) - (let ((l1_s3 (mod l1_s1 l1_s2))) - (let ((l1_s5 (>= l1_s1 l1_s4))) - (let ((l1_s6 (= l1_s3 l1_s4))) - (let ((l1_s7 (or l1_s5 l1_s6))) - (let ((l1_s9 (ite l1_s7 l1_s4 l1_s8))) - (let ((l1_s10 (* l1_s2 l1_s9))) - (let ((l1_s11 (- l1_s3 l1_s10))) - (let ((l1_s12 (> l1_s11 l1_s4))) - (let ((l1_s13 (< l1_s11 l1_s4))) - (let ((l1_s15 (ite l1_s13 l1_s14 l1_s11))) - (let ((l1_s16 (ite l1_s12 l1_s8 l1_s15))) - (let ((l1_s17 (= l1_s14 l1_s16))) - (let ((l1_s18 (+ l1_s2 l1_s11))) - (let ((l1_s19 (ite l1_s17 l1_s18 l1_s11))) - (let ((l1_s20 (= l1_s4 l1_s19))) - (let ((l1_s21 (and l1_s0 l1_s20))) - l1_s21))))))))))))))))))))) true s0)) +[GOOD] (define-fun s4 () Bool (|sbv.seqAll_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0)) [GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- diff --git a/SBVTestSuite/GoldFiles/lambda29.gold b/SBVTestSuite/GoldFiles/lambda29.gold index f09cf40d7..34f5ff96c 100644 --- a/SBVTestSuite/GoldFiles/lambda29.gold +++ b/SBVTestSuite/GoldFiles/lambda29.gold @@ -8,7 +8,7 @@ [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] (set-logic ALL) ; has lambda expressions, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -20,31 +20,35 @@ [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- SBV Function definitions +[GOOD] (define-fun-rec |sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool + (ite (= lst (as seq.empty (Seq Int))) + false + (or (select (lambda ((l1_s0 Int)) + (let ((l1_s1 2)) + (let ((l1_s3 0)) + (let ((l1_s7 1)) + (let ((l1_s13 (- 1))) + (let ((l1_s2 (mod l1_s0 l1_s1))) + (let ((l1_s4 (>= l1_s0 l1_s3))) + (let ((l1_s5 (= l1_s2 l1_s3))) + (let ((l1_s6 (or l1_s4 l1_s5))) + (let ((l1_s8 (ite l1_s6 l1_s3 l1_s7))) + (let ((l1_s9 (* l1_s1 l1_s8))) + (let ((l1_s10 (- l1_s2 l1_s9))) + (let ((l1_s11 (> l1_s10 l1_s3))) + (let ((l1_s12 (< l1_s10 l1_s3))) + (let ((l1_s14 (ite l1_s12 l1_s13 l1_s10))) + (let ((l1_s15 (ite l1_s11 l1_s7 l1_s14))) + (let ((l1_s16 (= l1_s13 l1_s15))) + (let ((l1_s17 (+ l1_s1 l1_s10))) + (let ((l1_s18 (ite l1_s16 l1_s17 l1_s10))) + (let ((l1_s19 (distinct l1_s3 l1_s18))) + l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))))) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) -[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int)) - (let ((l1_s2 2)) - (let ((l1_s4 0)) - (let ((l1_s8 1)) - (let ((l1_s14 (- 1))) - (let ((l1_s3 (mod l1_s1 l1_s2))) - (let ((l1_s5 (>= l1_s1 l1_s4))) - (let ((l1_s6 (= l1_s3 l1_s4))) - (let ((l1_s7 (or l1_s5 l1_s6))) - (let ((l1_s9 (ite l1_s7 l1_s4 l1_s8))) - (let ((l1_s10 (* l1_s2 l1_s9))) - (let ((l1_s11 (- l1_s3 l1_s10))) - (let ((l1_s12 (> l1_s11 l1_s4))) - (let ((l1_s13 (< l1_s11 l1_s4))) - (let ((l1_s15 (ite l1_s13 l1_s14 l1_s11))) - (let ((l1_s16 (ite l1_s12 l1_s8 l1_s15))) - (let ((l1_s17 (= l1_s14 l1_s16))) - (let ((l1_s18 (+ l1_s2 l1_s11))) - (let ((l1_s19 (ite l1_s17 l1_s18 l1_s11))) - (let ((l1_s20 (distinct l1_s4 l1_s19))) - (let ((l1_s21 (or l1_s0 l1_s20))) - l1_s21))))))))))))))))))))) false s0)) +[GOOD] (define-fun s4 () Bool (|sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0)) [GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- diff --git a/SBVTestSuite/GoldFiles/lambda30.gold b/SBVTestSuite/GoldFiles/lambda30.gold index b7a79e15c..f07e69138 100644 --- a/SBVTestSuite/GoldFiles/lambda30.gold +++ b/SBVTestSuite/GoldFiles/lambda30.gold @@ -8,7 +8,7 @@ [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] (set-logic ALL) ; has lambda expressions, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- @@ -20,31 +20,35 @@ [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- SBV Function definitions +[GOOD] (define-fun-rec |sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) Bool + (ite (= lst (as seq.empty (Seq Int))) + false + (or (select (lambda ((l1_s0 Int)) + (let ((l1_s1 2)) + (let ((l1_s3 0)) + (let ((l1_s7 1)) + (let ((l1_s13 (- 1))) + (let ((l1_s2 (mod l1_s0 l1_s1))) + (let ((l1_s4 (>= l1_s0 l1_s3))) + (let ((l1_s5 (= l1_s2 l1_s3))) + (let ((l1_s6 (or l1_s4 l1_s5))) + (let ((l1_s8 (ite l1_s6 l1_s3 l1_s7))) + (let ((l1_s9 (* l1_s1 l1_s8))) + (let ((l1_s10 (- l1_s2 l1_s9))) + (let ((l1_s11 (> l1_s10 l1_s3))) + (let ((l1_s12 (< l1_s10 l1_s3))) + (let ((l1_s14 (ite l1_s12 l1_s13 l1_s10))) + (let ((l1_s15 (ite l1_s11 l1_s7 l1_s14))) + (let ((l1_s16 (= l1_s13 l1_s15))) + (let ((l1_s17 (+ l1_s1 l1_s10))) + (let ((l1_s18 (ite l1_s16 l1_s17 l1_s10))) + (let ((l1_s19 (= l1_s3 l1_s18))) + l1_s19)))))))))))))))))))) (seq.nth lst 0)) (|sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))))) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) -[GOOD] (define-fun s4 () Bool (seq.foldl (lambda ((l1_s0 Bool) (l1_s1 Int)) - (let ((l1_s2 2)) - (let ((l1_s4 0)) - (let ((l1_s8 1)) - (let ((l1_s14 (- 1))) - (let ((l1_s3 (mod l1_s1 l1_s2))) - (let ((l1_s5 (>= l1_s1 l1_s4))) - (let ((l1_s6 (= l1_s3 l1_s4))) - (let ((l1_s7 (or l1_s5 l1_s6))) - (let ((l1_s9 (ite l1_s7 l1_s4 l1_s8))) - (let ((l1_s10 (* l1_s2 l1_s9))) - (let ((l1_s11 (- l1_s3 l1_s10))) - (let ((l1_s12 (> l1_s11 l1_s4))) - (let ((l1_s13 (< l1_s11 l1_s4))) - (let ((l1_s15 (ite l1_s13 l1_s14 l1_s11))) - (let ((l1_s16 (ite l1_s12 l1_s8 l1_s15))) - (let ((l1_s17 (= l1_s14 l1_s16))) - (let ((l1_s18 (+ l1_s2 l1_s11))) - (let ((l1_s19 (ite l1_s17 l1_s18 l1_s11))) - (let ((l1_s20 (= l1_s4 l1_s19))) - (let ((l1_s21 (or l1_s0 l1_s20))) - l1_s21))))))))))))))))))))) false s0)) +[GOOD] (define-fun s4 () Bool (|sbv.seqAny_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0)) [GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- diff --git a/SBVTestSuite/GoldFiles/lambda31.gold b/SBVTestSuite/GoldFiles/lambda31.gold index 00e613fd7..409dec1b3 100644 --- a/SBVTestSuite/GoldFiles/lambda31.gold +++ b/SBVTestSuite/GoldFiles/lambda31.gold @@ -8,52 +8,54 @@ [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] (set-logic ALL) ; has lambda expressions, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7) (seq.unit 8) (seq.unit 9) (seq.unit 10))) -[GOOD] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Seq Int)) [GOOD] (declare-fun s1 () (Seq Int)) [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- SBV Function definitions +[GOOD] (define-fun-rec |sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) (Seq Int) + (ite (= lst (as seq.empty (Seq Int))) + (as seq.empty (Seq Int)) + (ite (select (lambda ((l1_s0 Int)) + (let ((l1_s1 2)) + (let ((l1_s3 0)) + (let ((l1_s7 1)) + (let ((l1_s13 (- 1))) + (let ((l1_s2 (mod l1_s0 l1_s1))) + (let ((l1_s4 (>= l1_s0 l1_s3))) + (let ((l1_s5 (= l1_s2 l1_s3))) + (let ((l1_s6 (or l1_s4 l1_s5))) + (let ((l1_s8 (ite l1_s6 l1_s3 l1_s7))) + (let ((l1_s9 (* l1_s1 l1_s8))) + (let ((l1_s10 (- l1_s2 l1_s9))) + (let ((l1_s11 (> l1_s10 l1_s3))) + (let ((l1_s12 (< l1_s10 l1_s3))) + (let ((l1_s14 (ite l1_s12 l1_s13 l1_s10))) + (let ((l1_s15 (ite l1_s11 l1_s7 l1_s14))) + (let ((l1_s16 (= l1_s13 l1_s15))) + (let ((l1_s17 (+ l1_s1 l1_s10))) + (let ((l1_s18 (ite l1_s16 l1_s17 l1_s10))) + (let ((l1_s19 (= l1_s3 l1_s18))) + l1_s19)))))))))))))))))))) (seq.nth lst 0)) + (seq.++ (seq.unit (seq.nth lst 0)) (|sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))) + (|sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))))) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) -[GOOD] (define-fun s5 () (Seq Int) (seq.foldl (lambda ((l1_s0 (Seq Int)) (l1_s1 Int)) - (let ((l1_s2 2)) - (let ((l1_s4 0)) - (let ((l1_s8 1)) - (let ((l1_s14 (- 1))) - (let ((l1_s22 (as seq.empty (Seq Int)))) - (let ((l1_s3 (mod l1_s1 l1_s2))) - (let ((l1_s5 (>= l1_s1 l1_s4))) - (let ((l1_s6 (= l1_s3 l1_s4))) - (let ((l1_s7 (or l1_s5 l1_s6))) - (let ((l1_s9 (ite l1_s7 l1_s4 l1_s8))) - (let ((l1_s10 (* l1_s2 l1_s9))) - (let ((l1_s11 (- l1_s3 l1_s10))) - (let ((l1_s12 (> l1_s11 l1_s4))) - (let ((l1_s13 (< l1_s11 l1_s4))) - (let ((l1_s15 (ite l1_s13 l1_s14 l1_s11))) - (let ((l1_s16 (ite l1_s12 l1_s8 l1_s15))) - (let ((l1_s17 (= l1_s14 l1_s16))) - (let ((l1_s18 (+ l1_s2 l1_s11))) - (let ((l1_s19 (ite l1_s17 l1_s18 l1_s11))) - (let ((l1_s20 (= l1_s4 l1_s19))) - (let ((l1_s21 (seq.unit l1_s1))) - (let ((l1_s23 (ite l1_s20 l1_s21 l1_s22))) - (let ((l1_s24 (seq.++ l1_s0 l1_s23))) - l1_s24)))))))))))))))))))))))) s4 s0)) -[GOOD] (define-fun s6 () Bool (= s1 s5)) +[GOOD] (define-fun s4 () (Seq Int) (|sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(=_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0)) +[GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s3) -[GOOD] (assert s6) +[GOOD] (assert s5) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s1)) diff --git a/SBVTestSuite/GoldFiles/lambda32.gold b/SBVTestSuite/GoldFiles/lambda32.gold index 6b8e564d6..e6f699bb8 100644 --- a/SBVTestSuite/GoldFiles/lambda32.gold +++ b/SBVTestSuite/GoldFiles/lambda32.gold @@ -8,52 +8,54 @@ [GOOD] (set-option :pp.max_depth 4294967295) [GOOD] (set-option :pp.min_alias_size 4294967295) [GOOD] (set-option :model.inline_def true ) -[GOOD] (set-logic ALL) ; has unbounded values, using catch-all. +[GOOD] (set-logic ALL) ; has lambda expressions, using catch-all. [GOOD] ; --- uninterpreted sorts --- [GOOD] ; --- tuples --- [GOOD] ; --- sums --- [GOOD] ; --- literal constants --- [GOOD] (define-fun s2 () (Seq Int) (seq.++ (seq.unit 1) (seq.unit 2) (seq.unit 3) (seq.unit 4) (seq.unit 5) (seq.unit 6) (seq.unit 7) (seq.unit 8) (seq.unit 9) (seq.unit 10))) -[GOOD] (define-fun s4 () (Seq Int) (as seq.empty (Seq Int))) [GOOD] ; --- top level inputs --- [GOOD] (declare-fun s0 () (Seq Int)) [GOOD] (declare-fun s1 () (Seq Int)) [GOOD] ; --- constant tables --- [GOOD] ; --- non-constant tables --- [GOOD] ; --- uninterpreted constants --- +[GOOD] ; --- SBV Function definitions +[GOOD] (define-fun-rec |sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| ((lst (Seq Int))) (Seq Int) + (ite (= lst (as seq.empty (Seq Int))) + (as seq.empty (Seq Int)) + (ite (select (lambda ((l1_s0 Int)) + (let ((l1_s1 2)) + (let ((l1_s3 0)) + (let ((l1_s7 1)) + (let ((l1_s13 (- 1))) + (let ((l1_s2 (mod l1_s0 l1_s1))) + (let ((l1_s4 (>= l1_s0 l1_s3))) + (let ((l1_s5 (= l1_s2 l1_s3))) + (let ((l1_s6 (or l1_s4 l1_s5))) + (let ((l1_s8 (ite l1_s6 l1_s3 l1_s7))) + (let ((l1_s9 (* l1_s1 l1_s8))) + (let ((l1_s10 (- l1_s2 l1_s9))) + (let ((l1_s11 (> l1_s10 l1_s3))) + (let ((l1_s12 (< l1_s10 l1_s3))) + (let ((l1_s14 (ite l1_s12 l1_s13 l1_s10))) + (let ((l1_s15 (ite l1_s11 l1_s7 l1_s14))) + (let ((l1_s16 (= l1_s13 l1_s15))) + (let ((l1_s17 (+ l1_s1 l1_s10))) + (let ((l1_s18 (ite l1_s16 l1_s17 l1_s10))) + (let ((l1_s19 (distinct l1_s3 l1_s18))) + l1_s19)))))))))))))))))))) (seq.nth lst 0)) + (seq.++ (seq.unit (seq.nth lst 0)) (|sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))) + (|sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1)))))) [GOOD] ; --- user defined functions --- [GOOD] ; --- assignments --- [GOOD] (define-fun s3 () Bool (= s0 s2)) -[GOOD] (define-fun s5 () (Seq Int) (seq.foldl (lambda ((l1_s0 (Seq Int)) (l1_s1 Int)) - (let ((l1_s2 2)) - (let ((l1_s4 0)) - (let ((l1_s8 1)) - (let ((l1_s14 (- 1))) - (let ((l1_s22 (as seq.empty (Seq Int)))) - (let ((l1_s3 (mod l1_s1 l1_s2))) - (let ((l1_s5 (>= l1_s1 l1_s4))) - (let ((l1_s6 (= l1_s3 l1_s4))) - (let ((l1_s7 (or l1_s5 l1_s6))) - (let ((l1_s9 (ite l1_s7 l1_s4 l1_s8))) - (let ((l1_s10 (* l1_s2 l1_s9))) - (let ((l1_s11 (- l1_s3 l1_s10))) - (let ((l1_s12 (> l1_s11 l1_s4))) - (let ((l1_s13 (< l1_s11 l1_s4))) - (let ((l1_s15 (ite l1_s13 l1_s14 l1_s11))) - (let ((l1_s16 (ite l1_s12 l1_s8 l1_s15))) - (let ((l1_s17 (= l1_s14 l1_s16))) - (let ((l1_s18 (+ l1_s2 l1_s11))) - (let ((l1_s19 (ite l1_s17 l1_s18 l1_s11))) - (let ((l1_s20 (distinct l1_s4 l1_s19))) - (let ((l1_s21 (seq.unit l1_s1))) - (let ((l1_s23 (ite l1_s20 l1_s21 l1_s22))) - (let ((l1_s24 (seq.++ l1_s0 l1_s23))) - l1_s24)))))))))))))))))))))))) s4 s0)) -[GOOD] (define-fun s6 () Bool (= s1 s5)) +[GOOD] (define-fun s4 () (Seq Int) (|sbv.seqFilter_@SInteger_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s3_0))_(let_((l1_s7_1))_(let_((l1_s13_(-_1)))_(let_((l1_s2_(mod_l1_s0_l1_s1)))_(let_((l1_s4_(>=_l1_s0_l1_s3)))_(let_((l1_s5_(=_l1_s2_l1_s3)))_(let_((l1_s6_(or_l1_s4_l1_s5)))_(let_((l1_s8_(ite_l1_s6_l1_s3_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s8)))_(let_((l1_s10_(-_l1_s2_l1_s9)))_(let_((l1_s11_(>_l1_s10_l1_s3)))_(let_((l1_s12_(<_l1_s10_l1_s3)))_(let_((l1_s14_(ite_l1_s12_l1_s13_l1_s10)))_(let_((l1_s15_(ite_l1_s11_l1_s7_l1_s14)))_(let_((l1_s16_(=_l1_s13_l1_s15)))_(let_((l1_s17_(+_l1_s1_l1_s10)))_(let_((l1_s18_(ite_l1_s16_l1_s17_l1_s10)))_(let_((l1_s19_(distinct_l1_s3_l1_s18)))_l1_s19))))))))))))))))))))| s0)) +[GOOD] (define-fun s5 () Bool (= s1 s4)) [GOOD] ; --- delayedEqualities --- [GOOD] ; --- formula --- [GOOD] (assert s3) -[GOOD] (assert s6) +[GOOD] (assert s5) [SEND] (check-sat) [RECV] sat [SEND] (get-value (s1))