diff --git a/Data/SBV/Set.hs b/Data/SBV/Set.hs
index cbfce61fb..1dcb42ec7 100644
--- a/Data/SBV/Set.hs
+++ b/Data/SBV/Set.hs
@@ -145,8 +145,8 @@ complement ss
 --
 -- >>> prove $ \x (s :: SSet Integer) -> x `delete` (x `insert` s) .== s
 -- Falsifiable. Counter-example:
---   s0 =   2 :: Integer
---   s1 = {2} :: {Integer}
+--   s0 = 2 :: Integer
+--   s1 = U :: {Integer}
 --
 -- But the above is true if the element isn't in the set to start with:
 --
@@ -188,8 +188,8 @@ insert se ss
 --
 -- >>> prove $ \x (s :: SSet Integer) -> x `insert` (x `delete` s) .== s
 -- Falsifiable. Counter-example:
---   s0 =  2 :: Integer
---   s1 = {} :: {Integer}
+--   s0 =       2 :: Integer
+--   s1 = U - {2} :: {Integer}
 --
 -- But the above is true if the element is in the set to start with:
 --
diff --git a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
index c426fbbed..ef0e8f116 100644
--- a/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
+++ b/Documentation/SBV/Examples/Misc/FirstOrderLogic.hs
@@ -137,8 +137,8 @@ Falsifiable. Counter-example:
   P _   = False
 <BLANKLINE>
   Q :: U -> Bool
-  Q U_2 = False
   Q U_0 = False
+  Q U_2 = False
   Q _   = True
 
 The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call
diff --git a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
index e0f759bc8..c0121ab09 100644
--- a/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
+++ b/Documentation/SBV/Examples/WeakestPreconditions/Sum.hs
@@ -237,18 +237,14 @@ The other way we can have a bad measure is if it fails to decrease through the l
 >>> let invariant SumS{n, i, s} = s .== (i*(i+1)) `sDiv` 2 .&& i .<= n
 >>> let measure   SumS{n, i}    = [n + i]
 >>> void $ correctness invariant (Just measure)
-Following proof obligations failed:
-===================================
-  Measure for loop "i < n" is negative:
-    State  : SumS {n = 0, i = -1, s = 0}
-    Measure: -1
+Following proof obligation failed:
+==================================
   Measure for loop "i < n" does not decrease:
-    Before : SumS {n = 0, i = -1, s = 0}
-    Measure: -1
-    After  : SumS {n = 0, i = 0, s = 0}
-    Measure: 0
+    Before : SumS {n = 1, i = 0, s = 0}
+    Measure: 1
+    After  : SumS {n = 1, i = 1, s = 1}
+    Measure: 2
 
-Clearly, as @i@ increases, so does our bogus measure @n+i@. Note that in this case the counterexample has
-@i@ and @n@ as a negative value, as the SMT solver finds a counter-example to induction, not
-necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.
+Clearly, as @i@ increases, so does our bogus measure @n+i@. (Note that in this case the counterexample might have @i@ and @n@ as negative values, as the SMT solver finds a counter-example to induction, not
+necessarily a reachable state. Obviously, all such failures need to be addressed for the full proof.)
 -}
diff --git a/SBVTestSuite/GoldFiles/query1.gold b/SBVTestSuite/GoldFiles/query1.gold
index 2dc94ca4f..84221599f 100644
--- a/SBVTestSuite/GoldFiles/query1.gold
+++ b/SBVTestSuite/GoldFiles/query1.gold
@@ -74,7 +74,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "state of the most recent check-sat command is not known")
 [SEND] (get-info :version)
-[RECV] (:version "4.13.1")
+[RECV] (:version "4.13.4")
 [SEND] (get-info :status)
 [RECV] (:status sat)
 [GOOD] (define-fun s16 () Int 4)
@@ -105,7 +105,7 @@
 [SEND] (get-info :reason-unknown)
 [RECV] (:reason-unknown "unknown")
 [SEND] (get-info :version)
-[RECV] (:version "4.13.1")
+[RECV] (:version "4.13.4")
 [SEND] (get-info :memory)
 [RECV] unsupported
 [SEND] (get-info :time)
@@ -148,19 +148,19 @@
 [SEND] (get-proof)
 [RECV] ((set-logic ALL)
        (proof
-       (let (($x268 (<= s0 6)))
-       (let (($x269 (not $x268)))
-       (let (($x276 (or (not bey) $x269)))
-       (let ((@x274 (monotonicity (rewrite (= (> s0 6) $x269)) (= (=> bey (> s0 6)) (=> bey $x269)))))
-       (let ((@x280 (trans @x274 (rewrite (= (=> bey $x269) $x276)) (= (=> bey (> s0 6)) $x276))))
-       (let ((@x281 (mp (asserted (=> bey (> s0 6))) @x280 $x276)))
-       (let (($x293 (>= s0 6)))
-       (let (($x292 (not $x293)))
-       (let (($x300 (or (not hey) $x292)))
-       (let ((@x291 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x292)) (= (< s0 6) $x292))))
-       (let ((@x304 (trans (monotonicity @x291 (= (=> hey (< s0 6)) (=> hey $x292))) (rewrite (= (=> hey $x292) $x300)) (= (=> hey (< s0 6)) $x300))))
-       (let ((@x305 (mp (asserted (=> hey (< s0 6))) @x304 $x300)))
-       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x293 $x268)) (unit-resolution @x305 (asserted hey) $x292) (unit-resolution @x281 (asserted bey) $x269) false)))))))))))))))
+       (let (($x267 (<= s0 6)))
+       (let (($x268 (not $x267)))
+       (let (($x275 (or (not bey) $x268)))
+       (let ((@x273 (monotonicity (rewrite (= (> s0 6) $x268)) (= (=> bey (> s0 6)) (=> bey $x268)))))
+       (let ((@x279 (trans @x273 (rewrite (= (=> bey $x268) $x275)) (= (=> bey (> s0 6)) $x275))))
+       (let ((@x280 (mp (asserted (=> bey (> s0 6))) @x279 $x275)))
+       (let (($x292 (>= s0 6)))
+       (let (($x291 (not $x292)))
+       (let (($x299 (or (not hey) $x291)))
+       (let ((@x290 (trans (rewrite (= (< s0 6) (not (<= 6 s0)))) (rewrite (= (not (<= 6 s0)) $x291)) (= (< s0 6) $x291))))
+       (let ((@x303 (trans (monotonicity @x290 (= (=> hey (< s0 6)) (=> hey $x291))) (rewrite (= (=> hey $x291) $x299)) (= (=> hey (< s0 6)) $x299))))
+       (let ((@x304 (mp (asserted (=> hey (< s0 6))) @x303 $x299)))
+       (unit-resolution ((_ th-lemma arith farkas 1 1) (or $x292 $x267)) (unit-resolution @x304 (asserted hey) $x291) (unit-resolution @x280 (asserted bey) $x268) false)))))))))))))))
 [SEND, TimeOut: 90000ms] (get-assertions)
 
 [RECV] ((! s7 :named |a > 0|)
diff --git a/SBVTestSuite/GoldFiles/set_tupleSet.gold b/SBVTestSuite/GoldFiles/set_tupleSet.gold
index acaa3a740..e285dc61a 100644
--- a/SBVTestSuite/GoldFiles/set_tupleSet.gold
+++ b/SBVTestSuite/GoldFiles/set_tupleSet.gold
@@ -31,11 +31,12 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1) ((as const (Array Bool Bool)) true))))
+[RECV] ((s0 (mkSBVTuple2 (lambda ((x!1 Bool)) x!1)
+                    (store ((as const (Array Bool Bool)) false) false true))))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 
 FINAL:
 Satisfiable. Model:
-  s0 = ({True},U) :: ({Bool}, {Bool})
+  s0 = ({True},{False}) :: ({Bool}, {Bool})
 DONE!
diff --git a/SBVTestSuite/GoldFiles/set_uninterp1.gold b/SBVTestSuite/GoldFiles/set_uninterp1.gold
index 8363a8e07..ae89abe21 100644
--- a/SBVTestSuite/GoldFiles/set_uninterp1.gold
+++ b/SBVTestSuite/GoldFiles/set_uninterp1.gold
@@ -49,54 +49,54 @@ 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)))
+[RECV] ((s0 (store ((as const (Array E Bool)) false) B true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s5 () (Array E Bool) (store ((as const (Array E Bool)) true) A false))
+[GOOD] (define-fun s5 () (Array E Bool) (store ((as const (Array E Bool)) false) B true))
 [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 (store ((as const (Array E Bool)) true) C false) A false)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) C true) B true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) true) C false) A false))
+[GOOD] (define-fun s7 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) B true))
 [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)) false) B true) A true)))
+[RECV] ((s0 ((as const (Array E Bool)) true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s9 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A true))
+[GOOD] (define-fun s9 () (Array E Bool) ((as const (Array E Bool)) true))
 [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 (store ((as const (Array E Bool)) false) C true) A true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) false) B true) A true)))
 [GOOD] (push 1)
-[GOOD] (define-fun s11 () (Array E Bool) (store (store ((as const (Array E Bool)) false) C true) A true))
+[GOOD] (define-fun s11 () (Array E Bool) (store (store ((as const (Array E Bool)) false) B true) A 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)) true) B false) A false)))
+[RECV] ((s0 (store ((as const (Array E Bool)) true) B false)))
 [GOOD] (push 1)
-[GOOD] (define-fun s13 () (Array E Bool) (store (store ((as const (Array E Bool)) true) B false) A false))
+[GOOD] (define-fun s13 () (Array E Bool) (store ((as const (Array E Bool)) true) B false))
 [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 (store (store ((as const (Array E Bool)) false) C true) B true) A true)))
+[RECV] ((s0 (store (store ((as const (Array E Bool)) true) B false) A false)))
 [GOOD] (push 1)
-[GOOD] (define-fun s15 () (Array E Bool) (store (store (store ((as const (Array E Bool)) false) C true) B true) A true))
+[GOOD] (define-fun s15 () (Array E Bool) (store (store ((as const (Array E Bool)) true) B false) A false))
 [GOOD] (define-fun s16 () Bool (distinct s0 s15))
 [GOOD] (assert s16)
 Fast allSat, Looking for solution 9
@@ -115,17 +115,17 @@ Fast allSat, Looking for solution 9
 
 FINAL:
 Solution #1:
-  s0 = {A,B,C} :: {E}
-Solution #2:
   s0 = U - {A,B} :: {E}
+Solution #2:
+  s0 = U - {B} :: {E}
 Solution #3:
-  s0 = {A,C} :: {E}
-Solution #4:
   s0 = {A,B} :: {E}
+Solution #4:
+  s0 = U :: {E}
 Solution #5:
-  s0 = U - {A,C} :: {E}
+  s0 = {B,C} :: {E}
 Solution #6:
-  s0 = U - {A} :: {E}
+  s0 = {B} :: {E}
 Solution #7:
   s0 = {A} :: {E}
 Solution #8:
diff --git a/SBVTestSuite/GoldFiles/uiSat_test3.gold b/SBVTestSuite/GoldFiles/uiSat_test3.gold
index 72155b517..1bc153188 100644
--- a/SBVTestSuite/GoldFiles/uiSat_test3.gold
+++ b/SBVTestSuite/GoldFiles/uiSat_test3.gold
@@ -517,24 +517,20 @@ Looking for solution 18
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false)
-              true
-              false
-              false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
 [GOOD] (define-fun q1_model18 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model18_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model18 x!0))))
 [GOOD] (define-fun q2_model18 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) false
-          (ite (and (= x!0 true) (= x!1 true)) false
-          true))
+          (ite (and (= x!0 false) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model18_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -549,11 +545,14 @@ Looking for solution 19
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
+              true
+              false
+              true)))
 [GOOD] (define-fun q1_model19 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
+          (ite (and (= x!0 false)) true
           false)
        )
 [GOOD] (define-fun q1_model19_reject () Bool
@@ -561,8 +560,9 @@ Looking for solution 19
                   (distinct (q1         x!0)
                             (q1_model19 x!0))))
 [GOOD] (define-fun q2_model19 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model19_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -577,18 +577,19 @@ Looking for solution 20
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) false)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true false false)))
 [GOOD] (define-fun q1_model20 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model20_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model20 x!0))))
 [GOOD] (define-fun q2_model20 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
+          (ite (and (= x!0 true) (= x!1 false)) false
           true)
        )
 [GOOD] (define-fun q2_model20_reject () Bool
@@ -604,12 +605,12 @@ Looking for solution 21
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
 [SEND] (get-value (q2))
 [RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
 [GOOD] (define-fun q1_model21 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model21_reject () Bool
           (exists ((x!0 Bool))
@@ -631,23 +632,19 @@ Looking for solution 22
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) false)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false)
-              true
-              false
-              false)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
 [GOOD] (define-fun q1_model22 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model22_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model22 x!0))))
 [GOOD] (define-fun q2_model22 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) false
-          (ite (and (= x!0 true) (= x!1 true)) false
-          true))
+          true
        )
 [GOOD] (define-fun q2_model22_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -662,20 +659,18 @@ Looking for solution 23
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
 [GOOD] (define-fun q1_model23 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model23_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model23 x!0))))
 [GOOD] (define-fun q2_model23 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) true
-          false)
+          true
        )
 [GOOD] (define-fun q2_model23_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -690,24 +685,20 @@ Looking for solution 24
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
-              true
-              false
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
 [GOOD] (define-fun q1_model24 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model24_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model24 x!0))))
 [GOOD] (define-fun q2_model24 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) true
-          (ite (and (= x!0 false) (= x!1 false)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true)
        )
 [GOOD] (define-fun q2_model24_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -722,23 +713,19 @@ Looking for solution 25
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
-              true
-              false
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
 [GOOD] (define-fun q1_model25 ((x!0 Bool)) Bool
-          true
+          false
        )
 [GOOD] (define-fun q1_model25_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model25 x!0))))
 [GOOD] (define-fun q2_model25 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) true
-          (ite (and (= x!0 false) (= x!1 false)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true)
        )
 [GOOD] (define-fun q2_model25_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -753,11 +740,11 @@ Looking for solution 26
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 ((as const (Array Bool Bool Bool)) false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
 [GOOD] (define-fun q1_model26 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
+          (ite (and (= x!0 false)) true
           false)
        )
 [GOOD] (define-fun q1_model26_reject () Bool
@@ -765,7 +752,8 @@ Looking for solution 26
                   (distinct (q1         x!0)
                             (q1_model26 x!0))))
 [GOOD] (define-fun q2_model26 ((x!0 Bool) (x!1 Bool)) Bool
-          false
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true)
        )
 [GOOD] (define-fun q2_model26_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -782,7 +770,7 @@ Looking for solution 27
 [SEND] (get-value (q1))
 [RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
 [GOOD] (define-fun q1_model27 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -792,7 +780,7 @@ Looking for solution 27
                   (distinct (q1         x!0)
                             (q1_model27 x!0))))
 [GOOD] (define-fun q2_model27 ((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_model27_reject () Bool
@@ -808,20 +796,20 @@ Looking for solution 28
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model28 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model28_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model28 x!0))))
 [GOOD] (define-fun q2_model28 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 true)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model28_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -838,7 +826,7 @@ Looking for solution 29
 [SEND] (get-value (q1))
 [RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) false)))
 [GOOD] (define-fun q1_model29 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -848,8 +836,7 @@ Looking for solution 29
                   (distinct (q1         x!0)
                             (q1_model29 x!0))))
 [GOOD] (define-fun q2_model29 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) false
-          true)
+          false
        )
 [GOOD] (define-fun q2_model29_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -864,19 +851,20 @@ Looking for solution 30
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) false)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
 [GOOD] (define-fun q1_model30 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model30_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model30 x!0))))
 [GOOD] (define-fun q2_model30 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) false
-          true)
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model30_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -891,19 +879,20 @@ Looking for solution 31
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) false)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model31 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model31_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model31 x!0))))
 [GOOD] (define-fun q2_model31 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model31_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -918,24 +907,19 @@ Looking for solution 32
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false)
-              true
-              true
-              false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model32 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          false
        )
 [GOOD] (define-fun q1_model32_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model32 x!0))))
 [GOOD] (define-fun q2_model32 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
-          (ite (and (= x!0 false) (= x!1 false)) false
-          true))
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model32_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -952,10 +936,7 @@ Looking for solution 33
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
-              false
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model33 ((x!0 Bool)) Bool
           false
        )
@@ -964,9 +945,8 @@ Looking for solution 33
                   (distinct (q1         x!0)
                             (q1_model33 x!0))))
 [GOOD] (define-fun q2_model33 ((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))
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model33_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1010,7 +990,7 @@ Looking for solution 35
 [SEND] (get-value (q1))
 [RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model35 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -1020,7 +1000,7 @@ Looking for solution 35
                   (distinct (q1         x!0)
                             (q1_model35 x!0))))
 [GOOD] (define-fun q2_model35 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
+          (ite (and (= x!0 true) (= x!1 false)) true
           false)
        )
 [GOOD] (define-fun q2_model35_reject () Bool
@@ -1036,23 +1016,19 @@ Looking for solution 36
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) false)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
-              true
-              true
-              true)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) false)))
 [GOOD] (define-fun q1_model36 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model36_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model36 x!0))))
 [GOOD] (define-fun q2_model36 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
-          (ite (and (= x!0 false) (= x!1 true)) true
-          false))
+          false
        )
 [GOOD] (define-fun q2_model36_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1070,7 +1046,7 @@ Looking for solution 37
 [RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false)
-              false
+              true
               true
               false)))
 [GOOD] (define-fun q1_model37 ((x!0 Bool)) Bool
@@ -1082,7 +1058,7 @@ Looking for solution 37
                   (distinct (q1         x!0)
                             (q1_model37 x!0))))
 [GOOD] (define-fun q2_model37 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 true)) false
+          (ite (and (= x!0 true) (= x!1 true)) false
           (ite (and (= x!0 false) (= x!1 false)) false
           true))
        )
@@ -1101,9 +1077,9 @@ Looking for solution 38
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true)
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
+              true
               true
-              false
               true)))
 [GOOD] (define-fun q1_model38 ((x!0 Bool)) Bool
           false
@@ -1113,8 +1089,8 @@ Looking for solution 38
                   (distinct (q1         x!0)
                             (q1_model38 x!0))))
 [GOOD] (define-fun q2_model38 ((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
+          (ite (and (= x!0 false) (= x!1 true)) true
           false))
        )
 [GOOD] (define-fun q2_model38_reject () Bool
@@ -1130,24 +1106,19 @@ Looking for solution 39
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true)
-              false
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
 [GOOD] (define-fun q1_model39 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          false
        )
 [GOOD] (define-fun q1_model39_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model39 x!0))))
 [GOOD] (define-fun q2_model39 ((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))
+          false)
        )
 [GOOD] (define-fun q2_model39_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1162,24 +1133,24 @@ Looking for solution 40
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true)
-              false
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false)
               true
-              true)))
+              false
+              false)))
 [GOOD] (define-fun q1_model40 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model40_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model40 x!0))))
 [GOOD] (define-fun q2_model40 ((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))
+          (ite (and (= x!0 true) (= x!1 false)) false
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true))
        )
 [GOOD] (define-fun q2_model40_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1194,12 +1165,14 @@ Looking for solution 41
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
+              false
+              true
+              true)))
 [GOOD] (define-fun q1_model41 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          false
        )
 [GOOD] (define-fun q1_model41_reject () Bool
           (exists ((x!0 Bool))
@@ -1207,7 +1180,8 @@ Looking for solution 41
                             (q1_model41 x!0))))
 [GOOD] (define-fun q2_model41 ((x!0 Bool) (x!1 Bool)) Bool
           (ite (and (= x!0 false) (= x!1 true)) true
-          false)
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model41_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1222,11 +1196,12 @@ Looking for solution 42
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
 [GOOD] (define-fun q1_model42 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model42_reject () Bool
           (exists ((x!0 Bool))
@@ -1249,14 +1224,15 @@ Looking for solution 43
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
               true
               true
               true)))
 [GOOD] (define-fun q1_model43 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model43_reject () Bool
           (exists ((x!0 Bool))
@@ -1280,24 +1256,20 @@ Looking for solution 44
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
-              true
-              false
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
 [GOOD] (define-fun q1_model44 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model44_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model44 x!0))))
 [GOOD] (define-fun q2_model44 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) true
-          (ite (and (= x!0 false) (= x!1 true)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model44_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1312,20 +1284,20 @@ Looking for solution 45
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model45 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model45_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model45 x!0))))
 [GOOD] (define-fun q2_model45 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model45_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1340,19 +1312,24 @@ Looking for solution 46
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
+              true
+              true
+              true)))
 [GOOD] (define-fun q1_model46 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model46_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model46 x!0))))
 [GOOD] (define-fun q2_model46 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 true)) true
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model46_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1367,21 +1344,21 @@ Looking for solution 47
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false)
-              true
+              false
               true
               false)))
 [GOOD] (define-fun q1_model47 ((x!0 Bool)) Bool
-          true
+          false
        )
 [GOOD] (define-fun q1_model47_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model47 x!0))))
 [GOOD] (define-fun q2_model47 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
+          (ite (and (= x!0 false) (= x!1 true)) false
           (ite (and (= x!0 false) (= x!1 false)) false
           true))
        )
@@ -1398,19 +1375,24 @@ Looking for solution 48
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false)
+              false
+              true
+              false)))
 [GOOD] (define-fun q1_model48 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model48_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model48 x!0))))
 [GOOD] (define-fun q2_model48 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
-          true)
+          (ite (and (= x!0 false) (= x!1 true)) false
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true))
        )
 [GOOD] (define-fun q2_model48_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1425,18 +1407,23 @@ Looking for solution 49
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false)
+              true
+              false
+              false)))
 [GOOD] (define-fun q1_model49 ((x!0 Bool)) Bool
-          true
+          false
        )
 [GOOD] (define-fun q1_model49_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model49 x!0))))
 [GOOD] (define-fun q2_model49 ((x!0 Bool) (x!1 Bool)) Bool
-          true
+          (ite (and (= x!0 true) (= x!1 false)) false
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true))
        )
 [GOOD] (define-fun q2_model49_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1451,19 +1438,24 @@ Looking for solution 50
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
+              true
+              false
+              true)))
 [GOOD] (define-fun q1_model50 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model50_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model50 x!0))))
 [GOOD] (define-fun q2_model50 ((x!0 Bool) (x!1 Bool)) Bool
-          true
+          (ite (and (= x!0 true) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false))
        )
 [GOOD] (define-fun q2_model50_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1478,20 +1470,19 @@ Looking for solution 51
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true false false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model51 ((x!0 Bool)) Bool
-          (ite (and (= x!0 false)) true
-          false)
+          true
        )
 [GOOD] (define-fun q1_model51_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model51 x!0))))
 [GOOD] (define-fun q2_model51 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model51_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1508,7 +1499,10 @@ Looking for solution 52
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true false false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
+              true
+              true
+              true)))
 [GOOD] (define-fun q1_model52 ((x!0 Bool)) Bool
           true
        )
@@ -1517,8 +1511,9 @@ Looking for solution 52
                   (distinct (q1         x!0)
                             (q1_model52 x!0))))
 [GOOD] (define-fun q2_model52 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 true)) true
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model52_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1533,18 +1528,18 @@ Looking for solution 53
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
 [GOOD] (define-fun q1_model53 ((x!0 Bool)) Bool
-          false
+          true
        )
 [GOOD] (define-fun q1_model53_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model53 x!0))))
 [GOOD] (define-fun q2_model53 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
+          (ite (and (= x!0 false) (= x!1 false)) true
           false)
        )
 [GOOD] (define-fun q2_model53_reject () Bool
@@ -1560,20 +1555,23 @@ Looking for solution 54
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
+              false
+              true
+              true)))
 [GOOD] (define-fun q1_model54 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model54_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model54 x!0))))
 [GOOD] (define-fun q2_model54 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 true)) true
+          (ite (and (= x!0 false) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model54_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1588,24 +1586,19 @@ Looking for solution 55
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
-              true
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true false false)))
 [GOOD] (define-fun q1_model55 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model55_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model55 x!0))))
 [GOOD] (define-fun q2_model55 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
-          (ite (and (= x!0 true) (= x!1 false)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model55_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1622,10 +1615,7 @@ Looking for solution 56
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
-              true
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
 [GOOD] (define-fun q1_model56 ((x!0 Bool)) Bool
           true
        )
@@ -1635,8 +1625,7 @@ Looking for solution 56
                             (q1_model56 x!0))))
 [GOOD] (define-fun q2_model56 ((x!0 Bool) (x!1 Bool)) Bool
           (ite (and (= x!0 true) (= x!1 true)) true
-          (ite (and (= x!0 true) (= x!1 false)) true
-          false))
+          false)
        )
 [GOOD] (define-fun q2_model56_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1653,7 +1642,7 @@ Looking for solution 57
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
 [GOOD] (define-fun q1_model57 ((x!0 Bool)) Bool
           true
        )
@@ -1662,7 +1651,7 @@ Looking for solution 57
                   (distinct (q1         x!0)
                             (q1_model57 x!0))))
 [GOOD] (define-fun q2_model57 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 true)) true
           false)
        )
 [GOOD] (define-fun q2_model57_reject () Bool
@@ -1678,19 +1667,23 @@ Looking for solution 58
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 ((as const (Array Bool Bool Bool)) false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
+              true
+              false
+              true)))
 [GOOD] (define-fun q1_model58 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model58_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model58 x!0))))
 [GOOD] (define-fun q2_model58 ((x!0 Bool) (x!1 Bool)) Bool
-          false
+          (ite (and (= x!0 true) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false))
        )
 [GOOD] (define-fun q2_model58_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1705,20 +1698,24 @@ Looking for solution 59
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
+              false
+              false
+              true)))
 [GOOD] (define-fun q1_model59 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model59_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model59 x!0))))
 [GOOD] (define-fun q2_model59 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false))
        )
 [GOOD] (define-fun q2_model59_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1733,19 +1730,24 @@ Looking for solution 60
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 ((as const (Array Bool Bool)) true)))
+[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
+              false
+              false
+              true)))
 [GOOD] (define-fun q1_model60 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 false)) true
+          false)
        )
 [GOOD] (define-fun q1_model60_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model60 x!0))))
 [GOOD] (define-fun q2_model60 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false))
        )
 [GOOD] (define-fun q2_model60_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1762,7 +1764,7 @@ Looking for solution 61
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
 [GOOD] (define-fun q1_model61 ((x!0 Bool)) Bool
           true
        )
@@ -1771,8 +1773,8 @@ Looking for solution 61
                   (distinct (q1         x!0)
                             (q1_model61 x!0))))
 [GOOD] (define-fun q2_model61 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true)
        )
 [GOOD] (define-fun q2_model61_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1790,8 +1792,8 @@ Looking for solution 62
 [RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
-              false
               true
+              false
               true)))
 [GOOD] (define-fun q1_model62 ((x!0 Bool)) Bool
           true
@@ -1801,7 +1803,7 @@ Looking for solution 62
                   (distinct (q1         x!0)
                             (q1_model62 x!0))))
 [GOOD] (define-fun q2_model62 ((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
           (ite (and (= x!0 false) (= x!1 false)) true
           false))
        )
@@ -1818,24 +1820,19 @@ Looking for solution 63
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
-              false
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model63 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model63_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model63 x!0))))
 [GOOD] (define-fun q2_model63 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 true)) true
-          (ite (and (= x!0 false) (= x!1 false)) true
-          false))
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model63_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1850,20 +1847,23 @@ Looking for solution 64
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) true) true false)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true true false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false false false)
+              true
+              false
+              false)))
 [GOOD] (define-fun q1_model64 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model64_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model64 x!0))))
 [GOOD] (define-fun q2_model64 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 false)) false
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true))
        )
 [GOOD] (define-fun q2_model64_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1882,27 +1882,25 @@ Looking for solution 65
 
 RESULT: Solution #1:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True
+  q2 True  False = False
+  q2 False False = False
+  q2 _     _     = True
 Solution #2:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True  = True
-  q2 False False = True
-  q2 _     _     = False
+  q2 False False = False
+  q2 _     _     = True
 Solution #3:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True  = True
+  q2 True  False = True
   q2 False False = True
   q2 _     _     = False
 Solution #4:
@@ -1910,139 +1908,148 @@ Solution #4:
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = True
-  q2 _     _     = False
+  q2 True True = False
+  q2 _    _    = True
 Solution #5:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True
-  q2 _    _    = False
+  q2 False False = True
+  q2 False True  = True
+  q2 _     _     = False
 Solution #6:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 True = True
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True
-  q2 _    _    = False
+  q2 False False = True
+  q2 False True  = True
+  q2 _     _     = False
 Solution #7:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = False
+  q2 True  False = True
+  q2 False True  = True
+  q2 _     _     = False
 Solution #8:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True
-  q2 _    _     = False
+  q2 False True = True
+  q2 _     _    = False
 Solution #9:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True  = True
-  q2 True False = True
-  q2 _    _     = False
+  q2 True True = True
+  q2 _    _    = False
 Solution #10:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True  = True
-  q2 True False = True
-  q2 _    _     = False
+  q2 True False = False
+  q2 _    _     = True
 Solution #11:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True
-  q2 _    _     = False
+  q2 False True  = True
+  q2 False False = True
+  q2 _     _     = False
 Solution #12:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True
-  q2 _    _    = False
+  q2 False False = True
+  q2 _     _     = False
 Solution #13:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 _    _     = True
+  q2 True True  = True
+  q2 True False = True
+  q2 _    _     = False
 Solution #14:
   q1 :: Bool -> Bool
-  q1 False = True
-  q1 _     = False
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 _    _     = True
+  q2 True False = True
+  q2 _    _     = False
 Solution #15:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = True
+  q2 True  False = True
+  q2 False True  = True
+  q2 _     _     = False
 Solution #16:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = True
+  q2 True False = False
+  q2 True True  = False
+  q2 _    _     = True
 Solution #17:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = True
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True
+  q2 False True  = False
+  q2 False False = False
+  q2 _     _     = True
 Solution #18:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  True  = False
+  q2 False True  = False
   q2 False False = False
   q2 _     _     = True
 Solution #19:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = False
-  q2 _     _     = True
+  q2 True True  = True
+  q2 True False = True
+  q2 _    _     = False
 Solution #20:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = False
-  q2 _     _     = True
+  q2 True False = True
+  q2 _    _     = False
 Solution #21:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  False = True
-  q2 False True  = True
-  q2 _     _     = False
+  q2 True True = True
+  q2 _    _    = False
 Solution #22:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
   q2 True  True = True
@@ -2050,70 +2057,68 @@ Solution #22:
   q2 _     _    = False
 Solution #23:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
   q2 False True = True
   q2 _     _    = False
 Solution #24:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True
-  q2 _     _    = False
+  q2 False True  = True
+  q2 True  False = True
+  q2 _     _     = False
 Solution #25:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 True = True
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True
-  q2 True  True = True
-  q2 _     _    = False
+  q2 True  False = False
+  q2 False False = False
+  q2 _     _     = True
 Solution #26:
   q1 :: Bool -> Bool
-  q1 True = True
-  q1 _    = False
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True
-  q2 True  True = True
-  q2 _     _    = False
+  q2 True True = True
+  q2 _    _    = False
 Solution #27:
   q1 :: Bool -> Bool
   q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True
-  q2 True True  = True
-  q2 _    _     = False
+  q2 True  True = True
+  q2 False True = True
+  q2 _     _    = False
 Solution #28:
   q1 :: Bool -> Bool
   q1 True = True
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True  = False
+  q2 True  True  = False
   q2 False False = False
   q2 _     _     = True
 Solution #29:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  True = True
-  q2 False True = True
-  q2 _     _    = False
+  q2 _ _ = False
 Solution #30:
   q1 :: Bool -> Bool
   q1 True = True
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True
-  q2 _    _    = False
+  q2 True False = True
+  q2 _    _     = False
 Solution #31:
   q1 :: Bool -> Bool
   q1 _ = False
@@ -2126,127 +2131,122 @@ Solution #32:
   q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True  = True
-  q2 True  False = True
-  q2 _     _     = False
-Solution #33:
-  q1 :: Bool -> Bool
-  q1 True = True
-  q1 _    = False
-
-  q2 :: Bool -> Bool -> Bool
-  q2 True  True  = False
   q2 False False = False
   q2 _     _     = True
-Solution #34:
+Solution #33:
   q1 :: Bool -> Bool
   q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
   q2 True False = True
   q2 _    _     = False
-Solution #35:
+Solution #34:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 True = True
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
   q2 False False = False
   q2 _     _     = True
-Solution #36:
+Solution #35:
   q1 :: Bool -> Bool
   q1 True = True
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = False
-  q2 _     _     = True
-Solution #37:
+  q2 False True = True
+  q2 _     _    = False
+Solution #36:
   q1 :: Bool -> Bool
   q1 True = True
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True
-  q2 _     _    = False
+  q2 _ _ = False
+Solution #37:
+  q1 :: Bool -> Bool
+  q1 True = False
+  q1 _    = True
+
+  q2 :: Bool -> Bool -> Bool
+  q2 False False = False
+  q2 _     _     = True
 Solution #38:
   q1 :: Bool -> Bool
   q1 True = True
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True
-  q2 _    _     = False
+  q2 True True = True
+  q2 _    _    = False
 Solution #39:
   q1 :: Bool -> Bool
-  q1 True = True
-  q1 _    = False
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = False
+  q2 True True = False
+  q2 _    _    = True
 Solution #40:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  False = True
-  q2 False False = True
-  q2 _     _     = False
+  q2 True True = False
+  q2 _    _    = True
 Solution #41:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 True = True
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  False = True
-  q2 False False = True
-  q2 _     _     = False
+  q2 True True = False
+  q2 _    _    = True
 Solution #42:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = True
-  q2 _     _     = False
+  q2 _ _ = True
 Solution #43:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 True = True
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 True True  = False
-  q2 _    _     = True
+  q2 _ _ = True
 Solution #44:
   q1 :: Bool -> Bool
-  q1 True = True
-  q1 _    = False
+  q1 True = False
+  q1 _    = True
 
   q2 :: Bool -> Bool -> Bool
   q2 _ _ = True
 Solution #45:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 True = False
+  q1 _    = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True
+  q2 True False = False
+  q2 _    _     = True
 Solution #46:
   q1 :: Bool -> Bool
-  q1 True = True
-  q1 _    = False
+  q1 False = True
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True
+  q2 True  False = True
+  q2 False False = True
+  q2 _     _     = False
 Solution #47:
   q1 :: Bool -> Bool
-  q1 True = True
-  q1 _    = False
+  q1 True = False
+  q1 _    = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 True True  = False
-  q2 _    _     = True
+  q2 False False = True
+  q2 _     _     = False
 Solution #48:
   q1 :: Bool -> Bool
   q1 _ = False
diff --git a/SMTSolverVersions.md b/SMTSolverVersions.md
index 72877c322..307a42c67 100644
--- a/SMTSolverVersions.md
+++ b/SMTSolverVersions.md
@@ -33,7 +33,7 @@ report any issues you might see with newer releases.
       * Version 2.6.2 as downloaded from the above site on Apr 7, 2020
   * Z3:
       * http://github.com/Z3Prover/z3
-      * Version as downloaded from the above site on Sep 23rd, 2024
+      * Version as downloaded from the above site on Oct 10th, 2024
       * SBV typically relies on latest features of z3, so compiling directly
         from the sources is recommended. If that's not possible, you should
         always use their latest release.