adt_nested32.gold

** 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] ; --- 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 Mul Expr) ((as Val Expr) 1) ((as Add Expr) ((as Mul Expr) ((as Val Expr) 2) ((as Val Expr) 3)) ((as Mul Expr) ((as Val Expr) 4) ((as Val Expr) 5)))))
[GOOD] (define-fun s7 () Int 0)
[GOOD] (define-fun s21 () Int 1)
[GOOD] (define-fun s34 () Expr ((as Val Expr) 0))
[GOOD] (define-fun s68 () Expr ((as Val Expr) 26))
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () Expr)
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] (define-fun s3 () Bool ((as is-Add Bool) s0))
[GOOD] (define-fun s4 () Expr (getAdd_1 s0))
[GOOD] (define-fun s5 () Bool ((as is-Val Bool) s4))
[GOOD] (define-fun s6 () Int (getVal_1 s4))
[GOOD] (define-fun s8 () Bool (= s6 s7))
[GOOD] (define-fun s9 () Bool (and s5 s8))
[GOOD] (define-fun s10 () Bool (and s3 s9))
[GOOD] (define-fun s11 () Expr (getAdd_2 s0))
[GOOD] (define-fun s12 () Bool ((as is-Val Bool) s11))
[GOOD] (define-fun s13 () Int (getVal_1 s11))
[GOOD] (define-fun s14 () Bool (= s7 s13))
[GOOD] (define-fun s15 () Bool (and s12 s14))
[GOOD] (define-fun s16 () Bool (and s3 s15))
[GOOD] (define-fun s17 () Bool ((as is-Mul Bool) s0))
[GOOD] (define-fun s18 () Expr (getMul_1 s0))
[GOOD] (define-fun s19 () Bool ((as is-Val Bool) s18))
[GOOD] (define-fun s20 () Int (getVal_1 s18))
[GOOD] (define-fun s22 () Bool (= s20 s21))
[GOOD] (define-fun s23 () Bool (and s19 s22))
[GOOD] (define-fun s24 () Bool (and s17 s23))
[GOOD] (define-fun s25 () Expr (getMul_2 s0))
[GOOD] (define-fun s26 () Bool ((as is-Val Bool) s25))
[GOOD] (define-fun s27 () Int (getVal_1 s25))
[GOOD] (define-fun s28 () Bool (= s21 s27))
[GOOD] (define-fun s29 () Bool (and s26 s28))
[GOOD] (define-fun s30 () Bool (and s17 s29))
[GOOD] (define-fun s31 () Bool (= s7 s20))
[GOOD] (define-fun s32 () Bool (and s19 s31))
[GOOD] (define-fun s33 () Bool (and s17 s32))
[GOOD] (define-fun s35 () Expr (ite s33 s34 s0))
[GOOD] (define-fun s36 () Expr (ite s30 s18 s35))
[GOOD] (define-fun s37 () Expr (ite s24 s25 s36))
[GOOD] (define-fun s38 () Expr (ite s16 s4 s37))
[GOOD] (define-fun s39 () Expr (ite s10 s11 s38))
[GOOD] (define-fun s40 () Bool ((as is-Add Bool) s39))
[GOOD] (define-fun s41 () Expr (getAdd_1 s39))
[GOOD] (define-fun s42 () Bool ((as is-Mul Bool) s41))
[GOOD] (define-fun s43 () Expr (getMul_1 s41))
[GOOD] (define-fun s44 () Bool ((as is-Val Bool) s43))
[GOOD] (define-fun s45 () Expr (getMul_2 s41))
[GOOD] (define-fun s46 () Bool ((as is-Val Bool) s45))
[GOOD] (define-fun s47 () Expr (getAdd_2 s39))
[GOOD] (define-fun s48 () Bool ((as is-Mul Bool) s47))
[GOOD] (define-fun s49 () Expr (getMul_1 s47))
[GOOD] (define-fun s50 () Bool ((as is-Val Bool) s49))
[GOOD] (define-fun s51 () Expr (getMul_2 s47))
[GOOD] (define-fun s52 () Bool ((as is-Val Bool) s51))
[GOOD] (define-fun s53 () Bool (and s50 s52))
[GOOD] (define-fun s54 () Bool (and s48 s53))
[GOOD] (define-fun s55 () Bool (and s46 s54))
[GOOD] (define-fun s56 () Bool (and s44 s55))
[GOOD] (define-fun s57 () Bool (and s42 s56))
[GOOD] (define-fun s58 () Bool (and s40 s57))
[GOOD] (define-fun s59 () Int (getVal_1 s43))
[GOOD] (define-fun s60 () Int (getVal_1 s45))
[GOOD] (define-fun s61 () Int (* s59 s60))
[GOOD] (define-fun s62 () Int (getVal_1 s49))
[GOOD] (define-fun s63 () Int (getVal_1 s51))
[GOOD] (define-fun s64 () Int (* s62 s63))
[GOOD] (define-fun s65 () Int (+ s61 s64))
[GOOD] (define-fun s66 () Expr ((as Val Expr) s65))
[GOOD] (define-fun s67 () Expr (ite s58 s66 s39))
[GOOD] (define-fun s69 () Bool (distinct s67 s68))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s69)
[SEND] (check-sat)
[RECV] unsat
All good.
*** Solver   : Z3
*** Exit code: ExitSuccess