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-logic ALL) ; has user-defined sorts, using catch-all.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] (declare-datatypes ((E 0)) (((A) (B) (C))))
[GOOD] (define-fun E_constrIndex ((x E)) Int
          (ite (= x A) 0 (ite (= x B) 1 2))
       )
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (Array E Bool))
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
*** Checking Satisfiability, all solutions..
Looking for solution 1
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 ((as const (Array E Bool)) false)))
[GOOD] (define-fun s1 () (Array E Bool) ((as const (Array E Bool)) false))
[GOOD] (define-fun s2 () Bool (= s0 s1))
[GOOD] (define-fun s3 () Bool (not s2))
[GOOD] (assert s3)
Looking for solution 2
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (= x!1 B))))
[GOOD] (define-fun s4 () (Array E Bool) (store ((as const (Array E Bool)) false) B true))
[GOOD] (define-fun s5 () Bool (= s0 s4))
[GOOD] (define-fun s6 () Bool (not s5))
[GOOD] (assert s6)
Looking for solution 3
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 B) (= x!1 A)))))
[GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))
[GOOD] (define-fun s8 () Bool (= s0 s7))
[GOOD] (define-fun s9 () Bool (not s8))
[GOOD] (assert s9)
Looking for solution 4
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 B) (= x!1 C) (= x!1 A)))))
[GOOD] (define-fun s10 () (Array E Bool) (store (store (store ((as const (Array E Bool)) false) C true) B true) A true))
[GOOD] (define-fun s11 () Bool (= s0 s10))
[GOOD] (define-fun s12 () Bool (not s11))
[GOOD] (assert s12)
Looking for solution 5
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 B) (= x!1 C)))))
[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true))
[GOOD] (define-fun s14 () Bool (= s0 s13))
[GOOD] (define-fun s15 () Bool (not s14))
[GOOD] (assert s15)
Looking for solution 6
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (= x!1 A))))
[GOOD] (define-fun s16 () (Array E Bool) (store ((as const (Array E Bool)) false) A true))
[GOOD] (define-fun s17 () Bool (= s0 s16))
[GOOD] (define-fun s18 () Bool (not s17))
[GOOD] (assert s18)
Looking for solution 7
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (= x!1 C))))
[GOOD] (define-fun s19 () (Array E Bool) (store ((as const (Array E Bool)) false) C true))
[GOOD] (define-fun s20 () Bool (= s0 s19))
[GOOD] (define-fun s21 () Bool (not s20))
[GOOD] (assert s21)
Looking for solution 8
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 (lambda ((x!1 E)) (or (= x!1 A) (= x!1 C)))))
[GOOD] (define-fun s22 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))
[GOOD] (define-fun s23 () Bool (= s0 s22))
[GOOD] (define-fun s24 () Bool (not s23))
[GOOD] (assert s24)
Looking for solution 9
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess

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