** 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 q2 (Bool Bool) Bool)
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s0 () Bool (q2 false false))
*** Checking Satisfiability, all solutions..
[GOOD] (set-option :pp.max_depth      4294967295)
[GOOD] (set-option :pp.min_alias_size 4294967295)
Looking for solution 1
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 ((as const Array) false)))
[GOOD] (define-fun q2_model1 ((x!0 Bool) (x!1 Bool)) Bool
          false
       )
[GOOD] (define-fun q2_model1_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model1 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_1 () Bool q2_model1_reject)
[GOOD] (assert uiFunRejector_model_1)
Looking for solution 2
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 ((as const Array) true)))
[GOOD] (define-fun q2_model2 ((x!0 Bool) (x!1 Bool)) Bool
          true
       )
[GOOD] (define-fun q2_model2_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model2 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_2 () Bool q2_model2_reject)
[GOOD] (assert uiFunRejector_model_2)
Looking for solution 3
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) (not x!2))))))
[GOOD] (define-fun q2_model3 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model3_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model3 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_3 () Bool q2_model3_reject)
[GOOD] (assert uiFunRejector_model_3)
Looking for solution 4
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) x!2))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q2_model4 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model4_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model4 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_4 () Bool q2_model4_reject)
[GOOD] (assert uiFunRejector_model_4)
Looking for solution 5
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 x!2))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q2_model5 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) true
          false)
       )
[GOOD] (define-fun q2_model5_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model5 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_5 () Bool q2_model5_reject)
[GOOD] (assert uiFunRejector_model_5)
Looking for solution 6
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and x!1 (not x!2)) (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q2_model6 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model6_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model6 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_6 () Bool q2_model6_reject)
[GOOD] (assert uiFunRejector_model_6)
Looking for solution 7
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and x!1 (not x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q2_model7 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model7_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model7 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_7 () Bool q2_model7_reject)
[GOOD] (assert uiFunRejector_model_7)
Looking for solution 8
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (and x!1 (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q2_model8 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model8_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model8 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_8 () Bool q2_model8_reject)
[GOOD] (assert uiFunRejector_model_8)
Looking for solution 9
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (or (and (not x!1) x!2) (and x!1 x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) false))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q2_model9 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model9_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2        x!0 x!1)
                            (q2_model9 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_9 () Bool q2_model9_reject)
[GOOD] (assert uiFunRejector_model_9)
Looking for solution 10
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (and (not x!1) (not x!2)))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q2_model10 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          false)
       )
[GOOD] (define-fun q2_model10_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model10 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_10 () Bool q2_model10_reject)
[GOOD] (assert uiFunRejector_model_10)
Looking for solution 11
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and (not x!1) x!2)))))
[GOOD] (define-fun q2_model11 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model11_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model11 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_11 () Bool q2_model11_reject)
[GOOD] (assert uiFunRejector_model_11)
Looking for solution 12
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 (not x!2))) (not (and (not x!1) x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) true))
[GOOD] (define-fun q2_model12 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model12_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model12 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_12 () Bool q2_model12_reject)
[GOOD] (assert uiFunRejector_model_12)
Looking for solution 13
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (or (and x!1 (not x!2)) (and (not x!1) (not x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) false))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) true))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q2_model13 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 true) (= x!1 false)) true
          false))
       )
[GOOD] (define-fun q2_model13_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model13 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_13 () Bool q2_model13_reject)
[GOOD] (assert uiFunRejector_model_13)
Looking for solution 14
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool))
         (and (not (and x!1 (not x!2))) (not (and x!1 x!2))))))
[SEND] (get-value ((q2 false false)))
[RECV] (((q2 false false) true))
[SEND] (get-value ((q2 false true)))
[RECV] (((q2 false true) true))
[SEND] (get-value ((q2 true false)))
[RECV] (((q2 true false) false))
[SEND] (get-value ((q2 true true)))
[RECV] (((q2 true true) false))
[GOOD] (define-fun q2_model14 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 false) (= x!1 false)) true
          (ite (and (= x!0 false) (= x!1 true)) true
          false))
       )
[GOOD] (define-fun q2_model14_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model14 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_14 () Bool q2_model14_reject)
[GOOD] (assert uiFunRejector_model_14)
Looking for solution 15
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 (not x!2))))))
[GOOD] (define-fun q2_model15 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 false)) false
          true)
       )
[GOOD] (define-fun q2_model15_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model15 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_15 () Bool q2_model15_reject)
[GOOD] (assert uiFunRejector_model_15)
Looking for solution 16
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (q2))
[RECV] ((q2 (lambda ((x!1 Bool) (x!2 Bool)) (not (and x!1 x!2)))))
[GOOD] (define-fun q2_model16 ((x!0 Bool) (x!1 Bool)) Bool
          (ite (and (= x!0 true) (= x!1 true)) false
          true)
       )
[GOOD] (define-fun q2_model16_reject () Bool
          (exists ((x!0 Bool) (x!1 Bool))
                  (distinct (q2         x!0 x!1)
                            (q2_model16 x!0 x!1))))
[GOOD] (define-fun uiFunRejector_model_16 () Bool q2_model16_reject)
[GOOD] (assert uiFunRejector_model_16)
Looking for solution 17
[SEND] (check-sat)
[RECV] unsat
*** Solver   : Z3
*** Exit code: ExitSuccess

RESULT: Solution #1:
  q2 :: Bool -> Bool -> Bool
  q2 _ _ = False
Solution #2:
  q2 :: Bool -> Bool -> Bool
  q2 _ _ = True
Solution #3:
  q2 :: Bool -> Bool -> Bool
  q2 False False = False
  q2 _     _     = True 
Solution #4:
  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 _     _    = False
Solution #5:
  q2 :: Bool -> Bool -> Bool
  q2 True True = True 
  q2 _    _    = False
Solution #6:
  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 True True  = True 
  q2 _    _     = False
Solution #7:
  q2 :: Bool -> Bool -> Bool
  q2 True False = True 
  q2 _    _     = False
Solution #8:
  q2 :: Bool -> Bool -> Bool
  q2 False True  = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #9:
  q2 :: Bool -> Bool -> Bool
  q2 False True = True 
  q2 True  True = True 
  q2 _     _    = False
Solution #10:
  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 _     _     = False
Solution #11:
  q2 :: Bool -> Bool -> Bool
  q2 False True = False
  q2 _     _    = True 
Solution #12:
  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  True  = True 
  q2 _     _     = False
Solution #13:
  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 True  False = True 
  q2 _     _     = False
Solution #14:
  q2 :: Bool -> Bool -> Bool
  q2 False False = True 
  q2 False True  = True 
  q2 _     _     = False
Solution #15:
  q2 :: Bool -> Bool -> Bool
  q2 True False = False
  q2 _    _     = True 
Solution #16:
  q2 :: Bool -> Bool -> Bool
  q2 True True = False
  q2 _    _    = True 
Found 16 different solutions.