set_uninterp1.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 user-defined data-types, using catch-all.
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- ADTs  --- 
[GOOD] ; User defined ADT: E
[GOOD] (declare-datatype E (
           (A)
           (B)
           (C)
       ))
[GOOD] ; --- literal constants ---
[GOOD] ; --- top level inputs ---
[GOOD] (declare-fun s0 () (Array E Bool))
[GOOD] ; --- constant tables ---
[GOOD] ; --- non-constant tables ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user defined functions ---
[GOOD] ; --- assignments ---
[GOOD] ; --- delayedEqualities ---
[GOOD] ; --- formula ---
*** Checking Satisfiability, all solutions..
Fast allSat, Looking for solution 1
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ((as const (Array E Bool)) false)))
[GOOD] (push 1)
[GOOD] (define-fun s1 () (Array E Bool) ((as const (Array E Bool)) false))
[GOOD] (define-fun s2 () Bool (distinct s0 s1))
[GOOD] (assert s2)
Fast allSat, Looking for solution 2
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ((as const (Array E Bool)) true)))
[GOOD] (push 1)
[GOOD] (define-fun s3 () (Array E Bool) ((as const (Array E Bool)) true))
[GOOD] (define-fun s4 () Bool (distinct s0 s3))
[GOOD] (assert s4)
Fast allSat, Looking for solution 3
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (store ((as const (Array E Bool)) true) A false)))
[GOOD] (push 1)
[GOOD] (define-fun s5 () (Array E Bool) (store ((as const (Array E Bool)) true) (as A E) false))
[GOOD] (define-fun s6 () Bool (distinct s0 s5))
[GOOD] (assert s6)
Fast allSat, Looking for solution 4
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (store ((as const (Array E Bool)) true) C false)))
[GOOD] (push 1)
[GOOD] (define-fun s7 () (Array E Bool) (store ((as const (Array E Bool)) true) (as C E) false))
[GOOD] (define-fun s8 () Bool (distinct s0 s7))
[GOOD] (assert s8)
Fast allSat, Looking for solution 5
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (store (store ((as const (Array E Bool)) true) C false) B false)))
[GOOD] (push 1)
[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) true) (as C E) false) (as B E) false))
[GOOD] (define-fun s10 () Bool (distinct s0 s9))
[GOOD] (assert s10)
Fast allSat, Looking for solution 6
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (store ((as const (Array E Bool)) false) C true)))
[GOOD] (push 1)
[GOOD] (define-fun s11 () (Array E Bool) (store ((as const (Array E Bool)) false) (as C E) true))
[GOOD] (define-fun s12 () Bool (distinct s0 s11))
[GOOD] (assert s12)
Fast allSat, Looking for solution 7
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) A true)))
[GOOD] (push 1)
[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) (as C E) true) (as A E) true))
[GOOD] (define-fun s14 () Bool (distinct s0 s13))
[GOOD] (assert s14)
Fast allSat, Looking for solution 8
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (store ((as const (Array E Bool)) false) B true)))
[GOOD] (push 1)
[GOOD] (define-fun s15 () (Array E Bool) (store ((as const (Array E Bool)) false) (as B E) true))
[GOOD] (define-fun s16 () Bool (distinct s0 s15))
[GOOD] (assert s16)
Fast allSat, Looking for solution 9
[SEND] (check-sat)
[RECV] unsat
[GOOD] (pop 1)
[GOOD] (pop 1)
[GOOD] (pop 1)
[GOOD] (pop 1)
[GOOD] (pop 1)
[GOOD] (pop 1)
[GOOD] (pop 1)
[GOOD] (pop 1)
*** Solver   : Z3
*** Exit code: ExitSuccess

FINAL:
Solution #1:
  s0 = {B} :: {E}
Solution #2:
  s0 = {A,C} :: {E}
Solution #3:
  s0 = {C} :: {E}
Solution #4:
  s0 = U - {B,C} :: {E}
Solution #5:
  s0 = U - {C} :: {E}
Solution #6:
  s0 = U - {A} :: {E}
Solution #7:
  s0 = U :: {E}
Solution #8:
  s0 = {} :: {E}
Found 8 different solutions.
DONE!