uiSat_test1.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-logic ALL) ; NB. User specified.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] (declare-fun q1 (Bool) Bool)
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s0 () Bool (q1 false))
*** Checking Satisfiability, all solutions..
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
[GOOD] (set-option :model.inline_def  true      )
Looking for solution 1
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 ((as const Array) false)))
[GOOD] (define-fun q1_model1 ((x!0 Bool)) Bool
          false
       )
[GOOD] (define-fun q1_model1_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model1 x!0))))
[GOOD] (define-fun uiFunRejector_model_1 () Bool q1_model1_reject)
[GOOD] (assert uiFunRejector_model_1)
Looking for solution 2
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 ((as const Array) true)))
[GOOD] (define-fun q1_model2 ((x!0 Bool)) Bool
          true
       )
[GOOD] (define-fun q1_model2_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model2 x!0))))
[GOOD] (define-fun uiFunRejector_model_2 () Bool q1_model2_reject)
[GOOD] (assert uiFunRejector_model_2)
Looking for solution 3
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (store ((as const Array) true) true false)))
[GOOD] (define-fun q1_model3 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) false
          true)
       )
[GOOD] (define-fun q1_model3_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model3 x!0))))
[GOOD] (define-fun uiFunRejector_model_3 () Bool q1_model3_reject)
[GOOD] (assert uiFunRejector_model_3)
Looking for solution 4
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q1))
[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
[GOOD] (define-fun q1_model4 ((x!0 Bool)) Bool
          (ite (and (= x!0 true)) true
          false)
       )
[GOOD] (define-fun q1_model4_reject () Bool
          (exists ((x!0 Bool))
                  (distinct (q1        x!0)
                            (q1_model4 x!0))))
[GOOD] (define-fun uiFunRejector_model_4 () Bool q1_model4_reject)
[GOOD] (assert uiFunRejector_model_4)
Looking for solution 5
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess

RESULT: Solution #1:
  q1 :: Bool -> Bool
  q1 True = True 
  q1 _    = False
Solution #2:
  q1 :: Bool -> Bool
  q1 True = False
  q1 _    = True 
Solution #3:
  q1 :: Bool -> Bool
  q1 _ = True
Solution #4:
  q1 :: Bool -> Bool
  q1 _ = False
Found 4 different solutions.