** 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 (par (nm val) (
           (Val (getVal_1 val))
           (Var (getVar_1 nm))
           (Add (getAdd_1 (Expr nm val)) (getAdd_2 (Expr nm val)))
           (Mul (getMul_1 (Expr nm val)) (getMul_2 (Expr nm val)))
           (Let (getLet_1 nm) (getLet_2 (Expr nm val)) (getLet_3 (Expr nm val)))
       )))
[GOOD] ; --- literal constants ---
[GOOD] (define-fun s1 () (Expr String Int) ((as Mul (Expr String Int)) ((as Val (Expr String Int)) 3) ((as Add (Expr String Int)) ((as Val (Expr String Int)) 3) ((as Val (Expr String Int)) 4))))
[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 String Int))
[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