sbv-14.0: SBVTestSuite/GoldFiles/adt_expr03.gold
[MEASURE] Verifying termination measures for: eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer), eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer), get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)
[MEASURE] Checking: eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): not in a multi-member cycle, skipping mutual check
[MEASURE] Passed (terminating): eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)
[MEASURE] Checking: eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): barified = "|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|"
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): Uninterpreted ops in DAG: [("|get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)|",2),("|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|",2),("|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|",2),("|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|",2),("|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|",2),("|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|",2),("|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)|",2)]
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): recursive calls found = 6
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): trying sbv.dt.size.Expr arg2
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): sbv.dt.size.Expr arg2 -> OK (structural recursion)
[MEASURE] eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer): sbv.dt.size.Expr arg2 -> OK
[MEASURE] Passed (terminating): eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)
[MEASURE] Checking: get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)
[MEASURE] get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer): barified = "|get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)|"
[MEASURE] get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer): Uninterpreted ops in DAG: [("|get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)|",2)]
[MEASURE] get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer): recursive calls found = 1
[MEASURE] get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer): trying length arg1
[MEASURE] replayDAG {get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)}: replaying 13 node(s)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[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] ; --- tuples ---
[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
((mkSBVTuple2 (proj_1_SBVTuple2 T1)
(proj_2_SBVTuple2 T2))))))
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s2 () Int 0)
[GOOD] (define-fun s3 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Seq (SBVTuple2 String Int))) ; tracks user variable "arg0"
[GOOD] (declare-fun s1 () String) ; tracks user variable "arg1"
[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Int (seq.len s0))
[GOOD] (define-fun s5 () Bool (= s2 s4))
[GOOD] (define-fun s6 () Bool (not s5))
[GOOD] (define-fun s7 () (SBVTuple2 String Int) (seq.nth s0 s2))
[GOOD] (define-fun s8 () String (proj_1_SBVTuple2 s7))
[GOOD] (define-fun s9 () Bool (= s1 s8))
[GOOD] (define-fun s10 () Bool (and s6 s9))
[GOOD] (define-fun s11 () Int (proj_2_SBVTuple2 s7))
[GOOD] (define-fun s12 () Int (- s4 s3))
[GOOD] (define-fun s13 () (Seq (SBVTuple2 String Int)) (seq.extract s0 s3 s12))
[GOOD] (define-fun s15 () Int (ite s10 s11 s14))
[GOOD] (define-fun s16 () Int (ite s5 s2 s15))
[GOOD] (define-fun s17 () Bool (>= s4 s2))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s17))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] replayDAG {get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)}: replaying 13 node(s)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[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] ; --- tuples ---
[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
((mkSBVTuple2 (proj_1_SBVTuple2 T1)
(proj_2_SBVTuple2 T2))))))
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s2 () Int 0)
[GOOD] (define-fun s3 () Int 1)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Seq (SBVTuple2 String Int))) ; tracks user variable "arg0"
[GOOD] (declare-fun s1 () String) ; tracks user variable "arg1"
[GOOD] (declare-fun s14 () Int) ; tracks user variable "__internal_sbv_s14"
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s4 () Int (seq.len s0))
[GOOD] (define-fun s5 () Bool (= s2 s4))
[GOOD] (define-fun s6 () Bool (not s5))
[GOOD] (define-fun s7 () (SBVTuple2 String Int) (seq.nth s0 s2))
[GOOD] (define-fun s8 () String (proj_1_SBVTuple2 s7))
[GOOD] (define-fun s9 () Bool (= s1 s8))
[GOOD] (define-fun s10 () Bool (and s6 s9))
[GOOD] (define-fun s11 () Int (proj_2_SBVTuple2 s7))
[GOOD] (define-fun s12 () Int (- s4 s3))
[GOOD] (define-fun s13 () (Seq (SBVTuple2 String Int)) (seq.extract s0 s3 s12))
[GOOD] (define-fun s15 () Int (ite s10 s11 s14))
[GOOD] (define-fun s16 () Int (ite s5 s2 s15))
[GOOD] (define-fun s17 () Int (seq.len s13))
[GOOD] (define-fun s18 () Bool (not s10))
[GOOD] (define-fun s19 () Bool (and s6 s18))
[GOOD] (define-fun s20 () Bool (> s4 s17))
[GOOD] (define-fun s21 () Bool (=> s19 s20))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert (not s21))
[SEND] (check-sat)
[RECV] unsat
*** Solver : Z3
*** Exit code: ExitSuccess
[MEASURE] get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer): length arg1 -> OK
[MEASURE] Passed (terminating): get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)
** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[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] ; --- tuples ---
[GOOD] (declare-datatypes ((SBVTuple2 2)) ((par (T1 T2)
((mkSBVTuple2 (proj_1_SBVTuple2 T1)
(proj_2_SBVTuple2 T2))))))
[GOOD] ; --- sums ---
[GOOD] ; --- ADTs ---
[GOOD] ; User defined ADT: Expr
[GOOD] (declare-datatype Expr (
(Val (getVal_1 Int))
(Var (getVar_1 String))
(Add (getAdd_1 Expr) (getAdd_2 Expr))
(Mul (getMul_1 Expr) (getMul_2 Expr))
(Let (getLet_1 String) (getLet_2 Expr) (getLet_3 Expr))
))
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () Expr ((as Let Expr) "a" ((as Mul Expr) ((as Val Expr) 3) ((as Add Expr) ((as Val Expr) 3) ((as Val Expr) 4))) ((as Add Expr) ((as Var Expr) "a") ((as Add Expr) ((as Val Expr) 3) ((as Val Expr) 4)))))
[GOOD] (define-fun s3 () (Seq (SBVTuple2 String Int)) (as seq.empty (Seq (SBVTuple2 String Int))))
[GOOD] (define-fun s5 () Int 28)
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Expr)
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; |get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)| :: [(SString, SInteger)] -> SString -> SInteger [Recursive]
[GOOD] (define-fun-rec |get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)| ((l2_s0 (Seq (SBVTuple2 String Int))) (l2_s1 String)) Int
(let ((l2_s3 0))
(let ((l2_s11 1))
(let ((l2_s2 (seq.len l2_s0)))
(let ((l2_s4 (= l2_s2 l2_s3)))
(let ((l2_s5 (not l2_s4)))
(let ((l2_s6 (seq.nth l2_s0 l2_s3)))
(let ((l2_s7 (proj_1_SBVTuple2 l2_s6)))
(let ((l2_s8 (= l2_s1 l2_s7)))
(let ((l2_s9 (and l2_s5 l2_s8)))
(let ((l2_s10 (proj_2_SBVTuple2 l2_s6)))
(let ((l2_s12 (- l2_s2 l2_s11)))
(let ((l2_s13 (seq.extract l2_s0 l2_s11 l2_s12)))
(let ((l2_s14 (|get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)| l2_s13 l2_s1)))
(let ((l2_s15 (ite l2_s9 l2_s10 l2_s14)))
(let ((l2_s16 (ite l2_s4 l2_s3 l2_s15)))
l2_s16))))))))))))))))
[GOOD] ; |eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| :: [(SString, SInteger)] -> Expr -> SInteger [Recursive] [Refers to: |get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)|]
[GOOD] (define-fun-rec |eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| ((l1_s0 (Seq (SBVTuple2 String Int))) (l1_s1 Expr)) Int
(let ((l1_s2 ((as is-Val Bool) l1_s1)))
(let ((l1_s3 (getVal_1 l1_s1)))
(let ((l1_s4 ((as is-Var Bool) l1_s1)))
(let ((l1_s5 (getVar_1 l1_s1)))
(let ((l1_s6 (|get @(SBV [([Char],Integer)] -> SBV [Char] -> SBV Integer)| l1_s0 l1_s5)))
(let ((l1_s7 ((as is-Add Bool) l1_s1)))
(let ((l1_s8 (getAdd_1 l1_s1)))
(let ((l1_s9 (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| l1_s0 l1_s8)))
(let ((l1_s10 (getAdd_2 l1_s1)))
(let ((l1_s11 (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| l1_s0 l1_s10)))
(let ((l1_s12 (+ l1_s9 l1_s11)))
(let ((l1_s13 ((as is-Mul Bool) l1_s1)))
(let ((l1_s14 (getMul_1 l1_s1)))
(let ((l1_s15 (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| l1_s0 l1_s14)))
(let ((l1_s16 (getMul_2 l1_s1)))
(let ((l1_s17 (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| l1_s0 l1_s16)))
(let ((l1_s18 (* l1_s15 l1_s17)))
(let ((l1_s19 (getLet_1 l1_s1)))
(let ((l1_s20 (getLet_2 l1_s1)))
(let ((l1_s21 (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| l1_s0 l1_s20)))
(let ((l1_s22 ((as mkSBVTuple2 (SBVTuple2 String Int)) l1_s19 l1_s21)))
(let ((l1_s23 (seq.unit l1_s22)))
(let ((l1_s24 (seq.++ l1_s23 l1_s0)))
(let ((l1_s25 (getLet_3 l1_s1)))
(let ((l1_s26 (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| l1_s24 l1_s25)))
(let ((l1_s27 (ite l1_s13 l1_s18 l1_s26)))
(let ((l1_s28 (ite l1_s7 l1_s12 l1_s27)))
(let ((l1_s29 (ite l1_s4 l1_s6 l1_s28)))
(let ((l1_s30 (ite l1_s2 l1_s3 l1_s29)))
l1_s30))))))))))))))))))))))))))))))
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] (define-fun s4 () Int (|eval @(SBV [([Char],Integer)] -> SBV Expr -> SBV Integer)| s3 s0))
[GOOD] (define-fun s6 () Bool (distinct s4 s5))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s6)
[SEND] (check-sat)
[RECV] unsat
All good.
*** Solver : Z3
*** Exit code: ExitSuccess