** 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 Let Expr) "a" ((as Add 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)))) ((as Let Expr) "a" ((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)))) ((as Add Expr) ((as Var Expr) "a") ((as Add Expr) ((as Val Expr) 3) ((as Val Expr) 4))))) ((as Mul Expr) ((as Var Expr) "a") ((as Var Expr) "a"))))
[GOOD] (define-fun s5 () String "a")
[GOOD] (define-fun s8 () Int 0)
[GOOD] (define-fun s9 () String "b")
[GOOD] (define-fun s11 () String "c")
[GOOD] (define-fun s15 () Int 1)
[GOOD] (define-fun s16 () Int 2)
[GOOD] (define-fun s19 () Int 10)
[GOOD] (define-fun s22 () Int 3)
[GOOD] (define-fun s25 () Int 4)
[GOOD] (define-fun s28 () Int 5)
[GOOD] (define-fun s29 () Int 6)
[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-Var Bool) s0))
[GOOD] (define-fun s4 () String (getVar_1 s0))
[GOOD] (define-fun s6 () Bool (= s4 s5))
[GOOD] (define-fun s7 () Bool (and s3 s6))
[GOOD] (define-fun s10 () Bool (= s4 s9))
[GOOD] (define-fun s12 () Bool (= s4 s11))
[GOOD] (define-fun s13 () Bool (or s10 s12))
[GOOD] (define-fun s14 () Bool (and s3 s13))
[GOOD] (define-fun s17 () Bool ((as is-Val Bool) s0))
[GOOD] (define-fun s18 () Int (getVal_1 s0))
[GOOD] (define-fun s20 () Bool (< s18 s19))
[GOOD] (define-fun s21 () Bool (and s17 s20))
[GOOD] (define-fun s23 () Bool (= s18 s19))
[GOOD] (define-fun s24 () Bool (and s17 s23))
[GOOD] (define-fun s26 () Bool (> s18 s19))
[GOOD] (define-fun s27 () Bool (and s17 s26))
[GOOD] (define-fun s30 () Int (ite s27 s28 s29))
[GOOD] (define-fun s31 () Int (ite s24 s25 s30))
[GOOD] (define-fun s32 () Int (ite s21 s22 s31))
[GOOD] (define-fun s33 () Int (ite s3 s16 s32))
[GOOD] (define-fun s34 () Int (ite s14 s15 s33))
[GOOD] (define-fun s35 () Int (ite s7 s8 s34))
[GOOD] (define-fun s36 () Bool (distinct s29 s35))
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
[GOOD] (assert s2)
[GOOD] (assert s36)
[SEND] (check-sat)
[RECV] unsat
All good.
*** Solver   : Z3
*** Exit code: ExitSuccess