diff --git a/Data/SBV.hs b/Data/SBV.hs
index 54b6c1220..b80d6b05b 100644
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -1297,15 +1297,15 @@ Q.E.D.
 Q.E.D.
 >>> prove $ roundTrip @Int32
 Falsifiable. Counter-example:
-  s0 = RoundNearestTiesToEven :: RoundingMode
-  s1 =              -16891903 :: Int32
+  s0 = RoundTowardNegative :: RoundingMode
+  s1 =          -536873931 :: Int32
 
 Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float:
 
->>> toRational (-16891903 :: Float)
-(-16891904) % 1
+>>> toRational (-536873931 :: Float)
+(-536873920) % 1
 
-Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as
+Note how the numerator is different, it is off by 11. This is hardly surprising, since floats become sparser as
 the magnitude increases to be able to cover all the integer values representable.
 
 >>> :{
@@ -1328,15 +1328,15 @@ Q.E.D.
 >>> prove $ roundTrip @Int64
 Falsifiable. Counter-example:
   s0 = RoundNearestTiesToEven :: RoundingMode
-  s1 =    -144678154135535600 :: Int64
+  s1 =   -9223372036854775538 :: Int64
 
 Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the
 integer value for all possible values:
 
->>> toRational (fromIntegral (-144678154135535600 :: Int64) :: Double)
-(-144678154135535616) % 1
+>>> toRational (fromIntegral (-9223372036854775538 :: Int64) :: Double)
+(-9223372036854775808) % 1
 
-In this case the numerator is off by 16.
+In this case the numerator is off by 270.
 -}
 
 -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both
diff --git a/Documentation/SBV/Examples/Misc/Floating.hs b/Documentation/SBV/Examples/Misc/Floating.hs
index 1d22a2233..16ba8c5e3 100644
--- a/Documentation/SBV/Examples/Misc/Floating.hs
+++ b/Documentation/SBV/Examples/Misc/Floating.hs
@@ -66,19 +66,19 @@ assocPlus x y z = x + (y + z) .== (x + y) + z
 --
 -- >>> assocPlusRegular
 -- Falsifiable. Counter-example:
---   x = -1.1529219e18 :: Float
---   y =  5.8411555e11 :: Float
---   z = -3.5919253e19 :: Float
+--   x = -1.7478492e-21 :: Float
+--   y =   9.693523e-27 :: Float
+--   z =   5.595795e-20 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let x = -1.1529219e18 :: Float
--- >>> let y =  5.8411555e11 :: Float
--- >>> let z = -3.5919253e19 :: Float
+-- >>> let x = -1.7478492e-21 :: Float
+-- >>> let y =   9.693523e-27 :: Float
+-- >>> let z =   5.595795e-20 :: Float
 -- >>> x + (y + z)
--- -3.7072176e19
+-- 5.4210105e-20
 -- >>> (x + y) + z
--- -3.707217e19
+-- 5.421011e-20
 --
 -- Note the difference in the results!
 assocPlusRegular :: IO ThmResult
@@ -100,13 +100,13 @@ assocPlusRegular = prove $ do [x, y, z] <- sFloats ["x", "y", "z"]
 --
 -- >>> nonZeroAddition
 -- Falsifiable. Counter-example:
---   a = 1.4495462e-36 :: Float
---   b =       4.5e-44 :: Float
+--   a = 7.135861e-8 :: Float
+--   b = 8.57579e-39 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a = 1.4495462e-36 :: Float
--- >>> let b =       4.5e-44 :: Float
+-- >>> let a = 7.135861e-8 :: Float
+-- >>> let b = 8.57579e-39 :: Float
 -- >>> a + b == a
 -- True
 -- >>> b == 0
@@ -129,11 +129,11 @@ nonZeroAddition = prove $ do [a, b] <- sFloats ["a", "b"]
 --
 -- >>> multInverse
 -- Falsifiable. Counter-example:
---   a = 7.156233e-24 :: Float
+--   a = -1.4991268e38 :: Float
 --
 -- Indeed, we have:
 --
--- >>> let a = 7.156233e-24 :: Float
+-- >>> let a = -1.4991268e38 :: Float
 -- >>> a * (1/a)
 -- 0.99999994
 multInverse :: IO ThmResult
@@ -155,28 +155,28 @@ multInverse = prove $ do a <- sFloat "a"
 --
 -- >>> roundingAdd
 -- Satisfiable. Model:
---   rm = RoundTowardPositive :: RoundingMode
---   x  =                -2.0 :: Float
---   y  =       1.2621775e-29 :: Float
+--   rm = RoundTowardZero :: RoundingMode
+--   x  =       1.7499695 :: Float
+--   y  =       1.2539366 :: Float
 --
 -- (Note that depending on your version of Z3, you might get a different result.)
 -- Unfortunately Haskell floats do not allow computation with arbitrary rounding modes, but SBV's
 -- 'SFloatingPoint' type does. We have:
 --
--- >>> fpAdd sRoundTowardPositive (-2.0) (1.2621775e-29) :: SFPSingle
--- -1.99999988 :: SFloatingPoint 8 24
--- >>> fpAdd sRoundNearestTiesToEven (-2.0) (1.2621775e-29) :: SFPSingle
--- -2.0 :: SFloatingPoint 8 24
+-- >>> fpAdd sRoundTowardZero 1.7499695 1.2539366 :: SFPSingle
+-- 3.00390601 :: SFloatingPoint 8 24
+-- >>> fpAdd sRoundNearestTiesToEven 1.7499695 1.2539366 :: SFPSingle
+-- 3.00390625 :: SFloatingPoint 8 24
 --
--- We can see why these two results are indeed different: The 'RoundTowardPositive'
--- (which rounds towards positive infinity) produces a larger result, closer to 0. Indeed, if we treat these numbers
+-- We can see why these two results are indeed different: The 'RoundTowardZero'
+-- (which rounds towards the origin) produces a smaller result, closer to 0. Indeed, if we treat these numbers
 -- as 'Double' values, we get:
 --
--- >>> (-2.0) + 1.2621775e-29 :: Double
--- -2.0
+-- >>>  1.7499695 + 1.2539366 :: Double
+-- 3.0039061
 --
 -- we see that the "more precise" result is smaller than what the 'Float' value is, justifying the
--- larger value with 'RoundTowardPositive'. A more detailed study is beyond our current scope, so we'll
+-- smaller value with 'RoundTowardZero. A more detailed study is beyond our current scope, so we'll
 -- merely note that floating point representation and semantics is indeed a thorny
 -- subject, and point to <http://ece.uwaterloo.ca/~dwharder/NumericalAnalysis/02Numerics/Double/paper.pdf> as
 -- an excellent guide.
diff --git a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
index 4c6dc8cbc..a41771910 100644
--- a/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
+++ b/Documentation/SBV/Examples/Uninterpreted/Multiply.hs
@@ -47,12 +47,12 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 -- >>> sat synthMul22
 -- Satisfiable. Model:
 --   mul22_hi :: Bool -> Bool -> Bool -> Bool -> Bool
---   mul22_hi True  True  False True  = True
 --   mul22_hi False True  True  True  = True
+--   mul22_hi True  True  False True  = True
 --   mul22_hi True  False False True  = True
+--   mul22_hi True  False True  True  = True
 --   mul22_hi False True  True  False = True
 --   mul22_hi True  True  True  False = True
---   mul22_hi True  False True  True  = True
 --   mul22_hi _     _     _     _     = False
 -- <BLANKLINE>
 --   mul22_lo :: Bool -> Bool -> Bool
@@ -67,12 +67,12 @@ mul22 (a1, a0) (b1, b0) = (mul22_hi, mul22_lo)
 --
 -- >>> :{
 -- mul22_hi :: (SBool, SBool, SBool, SBool) -> SBool
--- mul22_hi params = params `sElem` [ (sTrue,  sTrue,  sFalse, sTrue)
---                                  , (sFalse, sTrue,  sTrue,  sTrue)
+-- mul22_hi params = params `sElem` [ (sFalse, sTrue,  sTrue,  sTrue)
+--                                  , (sTrue,  sTrue,  sFalse, sTrue)
 --                                  , (sTrue,  sFalse, sFalse, sTrue)
+--                                  , (sTrue,  sFalse, sTrue,  sTrue)
 --                                  , (sFalse, sTrue,  sTrue,  sFalse)
 --                                  , (sTrue,  sTrue,  sTrue,  sFalse)
---                                  , (sTrue,  sFalse, sTrue,  sTrue)
 --                                  ]
 -- :}
 --
diff --git a/SBVTestSuite/GoldFiles/allSat6.gold b/SBVTestSuite/GoldFiles/allSat6.gold
index bfce22404..a8b19fb02 100644
--- a/SBVTestSuite/GoldFiles/allSat6.gold
+++ b/SBVTestSuite/GoldFiles/allSat6.gold
@@ -1,8 +1,8 @@
 Solution #1:
-  x = 0 :: Word8
+  x = 1 :: Word8
   y = 2 :: Word8
 Solution #2:
-  x = 1 :: Word8
+  x = 0 :: Word8
   y = 2 :: Word8
 Solution #3:
   x = 0 :: Word8
diff --git a/SBVTestSuite/GoldFiles/uiSat_test2.gold b/SBVTestSuite/GoldFiles/uiSat_test2.gold
index 01a74a844..d7f934846 100644
--- a/SBVTestSuite/GoldFiles/uiSat_test2.gold
+++ b/SBVTestSuite/GoldFiles/uiSat_test2.gold
@@ -123,13 +123,13 @@ Looking for solution 7
 [SEND] (check-sat)
 [RECV] sat
 [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
               false
               true)))
 [GOOD] (define-fun q2_model7 ((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_model7_reject () Bool
@@ -142,14 +142,10 @@ Looking for solution 8
 [SEND] (check-sat)
 [RECV] sat
 [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 false true)))
 [GOOD] (define-fun q2_model8 ((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))
+          false)
        )
 [GOOD] (define-fun q2_model8_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -161,10 +157,14 @@ Looking for solution 9
 [SEND] (check-sat)
 [RECV] sat
 [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) true false true)
+              true
+              true
+              true)))
 [GOOD] (define-fun q2_model9 ((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_model9_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -176,14 +176,10 @@ Looking for solution 10
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false true false)
-              true
-              false
-              false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
 [GOOD] (define-fun q2_model10 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) false
-          (ite (and (= x!0 false) (= x!1 true)) false
-          true))
+          (ite (and (= x!0 false) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model10_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -195,10 +191,14 @@ Looking for solution 11
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
+              true
+              true
+              true)))
 [GOOD] (define-fun q2_model11 ((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)
+          false))
        )
 [GOOD] (define-fun q2_model11_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -210,10 +210,14 @@ Looking for solution 12
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q2))
-[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false true false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false true false)
+              true
+              true
+              false)))
 [GOOD] (define-fun q2_model12 ((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
-          true)
+          true))
        )
 [GOOD] (define-fun q2_model12_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -225,14 +229,10 @@ Looking for solution 13
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) false true false)
-              true
-              true
-              false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false true false)))
 [GOOD] (define-fun q2_model13 ((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
-          true))
+          true)
        )
 [GOOD] (define-fun q2_model13_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -244,9 +244,9 @@ Looking for solution 14
 [SEND] (check-sat)
 [RECV] sat
 [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 q2_model14 ((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_model14_reject () Bool
@@ -259,13 +259,13 @@ Looking for solution 15
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false)
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true false false)
+              true
               true
-              false
               false)))
 [GOOD] (define-fun q2_model15 ((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
+          (ite (and (= x!0 true) (= x!1 false)) false
           true))
        )
 [GOOD] (define-fun q2_model15_reject () Bool
@@ -278,9 +278,9 @@ Looking for solution 16
 [SEND] (check-sat)
 [RECV] sat
 [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)) true) true true false)))
 [GOOD] (define-fun q2_model16 ((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)
        )
 [GOOD] (define-fun q2_model16_reject () Bool
@@ -297,49 +297,49 @@ Looking for solution 17
 
 RESULT: Solution #1:
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 _    _     = True 
+  q2 True True = False
+  q2 _    _    = True 
 Solution #2:
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
   q2 True True  = False
+  q2 True False = False
   q2 _    _     = True 
 Solution #3:
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True 
+  q2 True False = False
+  q2 _    _     = True 
 Solution #4:
   q2 :: Bool -> Bool -> Bool
-  q2 True  True = False
   q2 False True = False
   q2 _     _    = True 
 Solution #5:
   q2 :: Bool -> Bool -> Bool
+  q2 True  True = False
   q2 False True = False
   q2 _     _    = True 
 Solution #6:
   q2 :: Bool -> Bool -> Bool
+  q2 True  True  = True 
   q2 False False = True 
   q2 _     _     = False
 Solution #7:
   q2 :: Bool -> Bool -> Bool
-  q2 True  False = False
-  q2 False True  = False
-  q2 _     _     = True 
+  q2 False False = True 
+  q2 _     _     = False
 Solution #8:
   q2 :: Bool -> Bool -> Bool
+  q2 True True  = True 
   q2 True False = True 
   q2 _    _     = False
 Solution #9:
+  q2 :: Bool -> Bool -> Bool
+  q2 True False = True 
+  q2 _    _     = False
+Solution #10:
   q2 :: Bool -> Bool -> Bool
   q2 True  False = True 
   q2 False True  = True 
   q2 _     _     = False
-Solution #10:
-  q2 :: Bool -> Bool -> Bool
-  q2 True False = True 
-  q2 True True  = True 
-  q2 _    _     = False
 Solution #11:
   q2 :: Bool -> Bool -> Bool
   q2 True True = True 
diff --git a/SBVTestSuite/GoldFiles/uiSat_test3.gold b/SBVTestSuite/GoldFiles/uiSat_test3.gold
index e07e29b06..f2967c9c4 100644
--- a/SBVTestSuite/GoldFiles/uiSat_test3.gold
+++ b/SBVTestSuite/GoldFiles/uiSat_test3.gold
@@ -520,20 +520,24 @@ Looking for solution 18
 [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) false false true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true true false)
+              true
+              false
+              false)))
 [GOOD] (define-fun q1_model18 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 true)) true
+          false)
        )
 [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 false) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 true) (= x!1 false)) false
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true))
        )
 [GOOD] (define-fun q2_model18_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -548,14 +552,11 @@ Looking for solution 19
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
+[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_model19 ((x!0 Bool)) Bool
-          (ite (and (= x!0 false)) true
+          (ite (and (= x!0 true)) true
           false)
        )
 [GOOD] (define-fun q1_model19_reject () Bool
@@ -563,9 +564,8 @@ 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 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_model19_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -607,11 +607,11 @@ Looking for solution 21
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false 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 ((as const (Array Bool Bool Bool)) true)))
 [GOOD] (define-fun q1_model21 ((x!0 Bool)) Bool
-          (ite (and (= x!0 false)) true
+          (ite (and (= x!0 true)) true
           false)
        )
 [GOOD] (define-fun q1_model21_reject () Bool
@@ -619,8 +619,7 @@ Looking for solution 21
                   (distinct (q1         x!0)
                             (q1_model21 x!0))))
 [GOOD] (define-fun q2_model21 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q2_model21_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -635,19 +634,23 @@ Looking for solution 22
 [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)) 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_model22 ((x!0 Bool)) Bool
-          (ite (and (= x!0 false)) true
-          false)
+          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
-          true
+          (ite (and (= x!0 true) (= x!1 false)) false
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true))
        )
 [GOOD] (define-fun q2_model22_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -662,19 +665,20 @@ Looking for solution 23
 [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)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
 [GOOD] (define-fun q1_model23 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          (ite (and (= x!0 true)) false
+          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
-          true
+          (ite (and (= x!0 false) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model23_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -689,20 +693,24 @@ Looking for solution 24
 [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)) 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_model24 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          (ite (and (= x!0 true)) false
+          true)
        )
 [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 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_model24_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -717,24 +725,23 @@ Looking for solution 25
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
+[RECV] ((q1 ((as const (Array Bool Bool)) true)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (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
-              false)))
+              true)))
 [GOOD] (define-fun q1_model25 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          true
        )
 [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)) false
-          (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_model25_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -751,7 +758,7 @@ Looking for solution 26
 [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_model26 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -761,8 +768,7 @@ Looking for solution 26
                   (distinct (q1         x!0)
                             (q1_model26 x!0))))
 [GOOD] (define-fun q2_model26 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 false) (= x!1 false)) false
-          true)
+          false
        )
 [GOOD] (define-fun q2_model26_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -779,10 +785,7 @@ Looking for solution 27
 [SEND] (get-value (q1))
 [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)
-              true
-              false
-              false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model27 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -792,9 +795,8 @@ 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)) 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_model27_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -811,7 +813,7 @@ Looking for solution 28
 [SEND] (get-value (q1))
 [RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [SEND] (get-value (q2))
-[RECV] ((q2 ((as const (Array Bool Bool Bool)) false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
 [GOOD] (define-fun q1_model28 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -821,7 +823,8 @@ Looking for solution 28
                   (distinct (q1         x!0)
                             (q1_model28 x!0))))
 [GOOD] (define-fun q2_model28 ((x!0 Bool) (x!1 Bool)) Bool
-          false
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model28_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -838,7 +841,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)) false) true false true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model29 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -848,8 +851,8 @@ 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 true) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model29_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -864,20 +867,19 @@ Looking for solution 30
 [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 ((as const (Array Bool Bool Bool)) false) true true true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model30 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          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 true) (= x!1 true)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model30_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -894,7 +896,7 @@ Looking for solution 31
 [SEND] (get-value (q1))
 [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 ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model31 ((x!0 Bool)) Bool
           false
        )
@@ -903,7 +905,7 @@ Looking for solution 31
                   (distinct (q1         x!0)
                             (q1_model31 x!0))))
 [GOOD] (define-fun q2_model31 ((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_model31_reject () Bool
@@ -919,19 +921,24 @@ Looking for solution 32
 [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 (store ((as const (Array Bool Bool Bool)) true) false false false)
+              true
+              true
+              false)))
 [GOOD] (define-fun q1_model32 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) true
+          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 false)) true
-          false)
+          (ite (and (= x!0 true) (= x!1 true)) false
+          (ite (and (= x!0 false) (= x!1 false)) false
+          true))
        )
 [GOOD] (define-fun q2_model32_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -948,7 +955,10 @@ Looking for solution 33
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [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)
+              false
+              true
+              true)))
 [GOOD] (define-fun q1_model33 ((x!0 Bool)) Bool
           false
        )
@@ -957,8 +967,9 @@ 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 false)) false
-          true)
+          (ite (and (= x!0 false) (= x!1 true)) true
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model33_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -973,12 +984,11 @@ Looking for solution 34
 [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 ((as const (Array Bool Bool Bool)) false) false true true)))
 [GOOD] (define-fun q1_model34 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          false
        )
 [GOOD] (define-fun q1_model34_reject () Bool
           (exists ((x!0 Bool))
@@ -1003,10 +1013,7 @@ Looking for solution 35
 [SEND] (get-value (q1))
 [RECV] ((q1 (lambda ((x!1 Bool)) x!1)))
 [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)) false) true true true)))
 [GOOD] (define-fun q1_model35 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) true
           false)
@@ -1016,9 +1023,8 @@ 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 false) (= x!1 true)) true
-          (ite (and (= x!0 true) (= x!1 false)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model35_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1035,7 +1041,10 @@ Looking for solution 36
 [SEND] (get-value (q1))
 [RECV] ((q1 ((as const (Array Bool Bool)) false)))
 [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)
+              true
+              true
+              true)))
 [GOOD] (define-fun q1_model36 ((x!0 Bool)) Bool
           false
        )
@@ -1045,7 +1054,8 @@ Looking for solution 36
                             (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
-          false)
+          (ite (and (= x!0 false) (= x!1 true)) true
+          false))
        )
 [GOOD] (define-fun q2_model36_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1060,21 +1070,22 @@ Looking for solution 37
 [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) false false false)
-              true
               false
+              true
               false)))
 [GOOD] (define-fun q1_model37 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) true
+          false)
        )
 [GOOD] (define-fun q1_model37_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model37 x!0))))
 [GOOD] (define-fun q2_model37 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 false)) false
+          (ite (and (= x!0 false) (= x!1 true)) false
           (ite (and (= x!0 false) (= x!1 false)) false
           true))
        )
@@ -1091,23 +1102,22 @@ Looking for solution 38
 [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 false true)
-              true
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true)
               true
+              false
               true)))
 [GOOD] (define-fun q1_model38 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) true
-          false)
+          false
        )
 [GOOD] (define-fun q1_model38_reject () Bool
           (exists ((x!0 Bool))
                   (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 true)) true
           (ite (and (= x!0 true) (= x!1 false)) true
+          (ite (and (= x!0 true) (= x!1 true)) true
           false))
        )
 [GOOD] (define-fun q2_model38_reject () Bool
@@ -1123,22 +1133,23 @@ Looking for solution 39
 [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)) false) true false true)
-              true
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true)
+              false
               true
               true)))
 [GOOD] (define-fun q1_model39 ((x!0 Bool)) Bool
-          false
+          (ite (and (= x!0 true)) true
+          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
-          (ite (and (= x!0 true) (= x!1 false)) true
           false))
        )
 [GOOD] (define-fun q2_model39_reject () Bool
@@ -1154,20 +1165,24 @@ Looking for solution 40
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
+[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) true false true)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true true true)
+              false
+              true
+              true)))
 [GOOD] (define-fun q1_model40 ((x!0 Bool)) Bool
-          (ite (and (= x!0 false)) true
-          false)
+          (ite (and (= x!0 true)) false
+          true)
        )
 [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 true) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 false) (= x!1 true)) true
+          (ite (and (= x!0 true) (= x!1 true)) true
+          false))
        )
 [GOOD] (define-fun q2_model40_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1182,24 +1197,20 @@ Looking for solution 41
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (q1))
-[RECV] ((q1 (store ((as const (Array Bool Bool)) false) false true)))
+[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)) false) true false true)
-              true
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false true true)))
 [GOOD] (define-fun q1_model41 ((x!0 Bool)) Bool
-          (ite (and (= x!0 false)) true
-          false)
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model41_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model41 x!0))))
 [GOOD] (define-fun q2_model41 ((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 false) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model41_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1216,7 +1227,7 @@ Looking for solution 42
 [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_model42 ((x!0 Bool)) Bool
           true
        )
@@ -1225,7 +1236,7 @@ Looking for solution 42
                   (distinct (q1         x!0)
                             (q1_model42 x!0))))
 [GOOD] (define-fun q2_model42 ((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_model42_reject () Bool
@@ -1243,7 +1254,7 @@ Looking for solution 43
 [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)
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
               true
               true
               true)))
@@ -1256,7 +1267,7 @@ Looking for solution 43
                             (q1_model43 x!0))))
 [GOOD] (define-fun q2_model43 ((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
+          (ite (and (= x!0 false) (= x!1 true)) true
           false))
        )
 [GOOD] (define-fun q2_model43_reject () Bool
@@ -1272,22 +1283,23 @@ Looking for solution 44
 [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)) true) true false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
-              false
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false true true)
               true
+              false
               true)))
 [GOOD] (define-fun q1_model44 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          true)
        )
 [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 false) (= x!1 true)) true
           (ite (and (= x!0 true) (= x!1 false)) true
+          (ite (and (= x!0 false) (= x!1 true)) true
           false))
        )
 [GOOD] (define-fun q2_model44_reject () Bool
@@ -1303,11 +1315,12 @@ Looking for solution 45
 [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)) true) true false)))
 [SEND] (get-value (q2))
 [RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model45 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model45_reject () Bool
           (exists ((x!0 Bool))
@@ -1332,10 +1345,7 @@ Looking for solution 46
 [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)
-              false
-              false
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) false false false)))
 [GOOD] (define-fun q1_model46 ((x!0 Bool)) Bool
           true
        )
@@ -1344,9 +1354,8 @@ Looking for solution 46
                   (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)) 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_model46_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1361,14 +1370,14 @@ Looking for solution 47
 [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 (store ((as const (Array Bool Bool Bool)) true) false false false)
               true
               true
               false)))
 [GOOD] (define-fun q1_model47 ((x!0 Bool)) Bool
-          false
+          true
        )
 [GOOD] (define-fun q1_model47_reject () Bool
           (exists ((x!0 Bool))
@@ -1392,19 +1401,19 @@ Looking for solution 48
 [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 ((as const (Array Bool Bool Bool)) true) true true false)))
 [GOOD] (define-fun q1_model48 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [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
-          false
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true)
        )
 [GOOD] (define-fun q2_model48_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1419,20 +1428,18 @@ Looking for solution 49
 [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 true true)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
 [GOOD] (define-fun q1_model49 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [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
-          (ite (and (= x!0 false) (= x!1 true)) true
-          false)
+          true
        )
 [GOOD] (define-fun q2_model49_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1449,7 +1456,7 @@ Looking for solution 50
 [SEND] (get-value (q1))
 [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) true true true)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
 [GOOD] (define-fun q1_model50 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) false
           true)
@@ -1459,8 +1466,7 @@ Looking for solution 50
                   (distinct (q1         x!0)
                             (q1_model50 x!0))))
 [GOOD] (define-fun q2_model50 ((x!0 Bool) (x!1 Bool)) Bool
-          (ite (and (= x!0 true) (= x!1 true)) true
-          false)
+          true
        )
 [GOOD] (define-fun q2_model50_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1475,24 +1481,20 @@ Looking for solution 51
 [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) true true true)
-              false
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true false false)))
 [GOOD] (define-fun q1_model51 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          (ite (and (= x!0 false)) true
+          false)
        )
 [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 false) (= x!1 true)) true
-          (ite (and (= x!0 true) (= x!1 true)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model51_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1509,10 +1511,7 @@ Looking for solution 52
 [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 true true)
-              false
-              true
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) true) true false false)))
 [GOOD] (define-fun q1_model52 ((x!0 Bool)) Bool
           true
        )
@@ -1521,9 +1520,8 @@ 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 false) (= x!1 true)) true
-          (ite (and (= x!0 true) (= x!1 true)) true
-          false))
+          (ite (and (= x!0 true) (= x!1 false)) false
+          true)
        )
 [GOOD] (define-fun q2_model52_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1538,18 +1536,18 @@ Looking for solution 53
 [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 ((as const (Array Bool Bool Bool)) false) false true true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
 [GOOD] (define-fun q1_model53 ((x!0 Bool)) Bool
-          true
+          false
        )
 [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 false) (= x!1 true)) true
+          (ite (and (= x!0 true) (= x!1 true)) true
           false)
        )
 [GOOD] (define-fun q2_model53_reject () Bool
@@ -1567,10 +1565,7 @@ Looking for solution 54
 [SEND] (get-value (q1))
 [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) false false false)
-              true
-              true
-              false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model54 ((x!0 Bool)) Bool
           (ite (and (= x!0 true)) false
           true)
@@ -1580,9 +1575,8 @@ Looking for solution 54
                   (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 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_model54_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1597,11 +1591,15 @@ Looking for solution 55
 [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)) true) true false)))
 [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) true false true)
+              true
+              true
+              true)))
 [GOOD] (define-fun q1_model55 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          true)
        )
 [GOOD] (define-fun q1_model55_reject () Bool
           (exists ((x!0 Bool))
@@ -1609,7 +1607,8 @@ Looking for solution 55
                             (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
-          false)
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model55_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1624,20 +1623,23 @@ Looking for solution 56
 [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) false false false)))
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) true false true)
+              true
+              true
+              true)))
 [GOOD] (define-fun q1_model56 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model56_reject () Bool
           (exists ((x!0 Bool))
                   (distinct (q1         x!0)
                             (q1_model56 x!0))))
 [GOOD] (define-fun q2_model56 ((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_model56_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1654,7 +1656,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)) true) true true false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true false true)))
 [GOOD] (define-fun q1_model57 ((x!0 Bool)) Bool
           true
        )
@@ -1663,8 +1665,8 @@ 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 true)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 false)) true
+          false)
        )
 [GOOD] (define-fun q2_model57_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1679,18 +1681,19 @@ Looking for solution 58
 [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)) true) true false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 ((as const (Array Bool Bool Bool)) true)))
+[RECV] ((q2 ((as const (Array Bool Bool Bool)) false)))
 [GOOD] (define-fun q1_model58 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          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
-          true
+          false
        )
 [GOOD] (define-fun q2_model58_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1705,19 +1708,20 @@ Looking for solution 59
 [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)) true) true false)))
 [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 true true)))
 [GOOD] (define-fun q1_model59 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          true)
        )
 [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 false)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model59_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1732,20 +1736,19 @@ Looking for solution 60
 [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 false false)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) true true true)))
 [GOOD] (define-fun q1_model60 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [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 false)) false
-          true)
+          (ite (and (= x!0 true) (= x!1 true)) true
+          false)
        )
 [GOOD] (define-fun q2_model60_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1760,14 +1763,11 @@ Looking for solution 61
 [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 (store ((as const (Array Bool Bool Bool)) false) false true true)
-              false
-              false
-              true)))
+[RECV] ((q2 (store ((as const (Array Bool Bool Bool)) false) false false true)))
 [GOOD] (define-fun q1_model61 ((x!0 Bool)) Bool
-          false
+          true
        )
 [GOOD] (define-fun q1_model61_reject () Bool
           (exists ((x!0 Bool))
@@ -1775,8 +1775,7 @@ Looking for solution 61
                             (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
-          (ite (and (= x!0 false) (= x!1 true)) true
-          false))
+          false)
        )
 [GOOD] (define-fun q2_model61_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1791,23 +1790,22 @@ Looking for solution 62
 [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 true true)
-              false
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
               false
+              true
               true)))
 [GOOD] (define-fun q1_model62 ((x!0 Bool)) Bool
-          (ite (and (= x!0 true)) false
-          true)
+          true
        )
 [GOOD] (define-fun q1_model62_reject () Bool
           (exists ((x!0 Bool))
                   (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 false)) true
           (ite (and (= x!0 false) (= x!1 true)) true
+          (ite (and (= x!0 false) (= x!1 false)) true
           false))
        )
 [GOOD] (define-fun q2_model62_reject () Bool
@@ -1823,23 +1821,24 @@ Looking for solution 63
 [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)) true) true false)))
 [SEND] (get-value (q2))
-[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) true) true false false)
-              true
+[RECV] ((q2 (store (store ((as const (Array Bool Bool Bool)) false) false false true)
+              false
               true
-              false)))
+              true)))
 [GOOD] (define-fun q1_model63 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          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 true) (= x!1 true)) false
-          (ite (and (= x!0 true) (= x!1 false)) false
-          true))
+          (ite (and (= x!0 false) (= x!1 true)) true
+          (ite (and (= x!0 false) (= x!1 false)) true
+          false))
        )
 [GOOD] (define-fun q2_model63_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1854,19 +1853,20 @@ Looking for solution 64
 [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)) true) true false)))
 [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_model64 ((x!0 Bool)) Bool
-          true
+          (ite (and (= x!0 true)) false
+          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 false) (= x!1 false)) true
-          false)
+          (ite (and (= x!0 true) (= x!1 true)) false
+          true)
        )
 [GOOD] (define-fun q2_model64_reject () Bool
           (exists ((x!0 Bool) (x!1 Bool))
@@ -1885,138 +1885,135 @@ Looking for solution 65
 
 RESULT: Solution #1:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = True 
-  q2 _     _     = False
+  q2 True True = False
+  q2 _    _    = True 
 Solution #2:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True  = False
-  q2 True False = False
-  q2 _    _     = True 
+  q2 False True  = True 
+  q2 False False = True 
+  q2 _     _     = False
 Solution #3:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = True 
   q2 False True  = True 
+  q2 False False = True 
   q2 _     _     = False
 Solution #4:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
   q2 False False = True 
-  q2 False True  = True 
   q2 _     _     = False
 Solution #5:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 _    _     = True 
+  q2 True True = True 
+  q2 _    _    = False
 Solution #6:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 _    _     = True 
+  q2 True True = True 
+  q2 _    _    = False
 Solution #7:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = True
+  q2 _ _ = False
 Solution #8:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True 
+  q2 True False = True 
+  q2 _    _     = False
 Solution #9:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = False
-  q2 _     _     = True 
+  q2 True True  = True 
+  q2 True False = True 
+  q2 _    _     = False
 Solution #10:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True 
-  q2 _    _    = False
+  q2 True True  = True 
+  q2 True False = True 
+  q2 _    _     = False
 Solution #11:
   q1 :: Bool -> Bool
   q1 True = False
   q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  True  = False
-  q2 False False = False
-  q2 _     _     = True 
+  q2 True False = True 
+  q2 _    _     = False
 Solution #12:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True 
-  q2 _     _    = False
+  q2 True True = True 
+  q2 _    _    = False
 Solution #13:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True 
-  q2 True  True = True 
-  q2 _     _    = False
+  q2 True False = False
+  q2 _    _     = True 
 Solution #14:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 False = True 
+  q1 _     = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True 
-  q2 True  True = True 
-  q2 _     _    = False
+  q2 True False = False
+  q2 _    _     = True 
 Solution #15:
   q1 :: Bool -> Bool
   q1 True = False
   q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True 
-  q2 _    _    = False
+  q2 _ _ = True
 Solution #16:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True 
-  q2 _     _    = False
+  q2 _ _ = True
 Solution #17:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = False
+  q2 True True = False
+  q2 _    _    = True 
 Solution #18:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
   q2 True  True  = False
@@ -2027,79 +2024,81 @@ Solution #19:
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = True 
-  q2 True  False = True 
-  q2 _     _     = False
+  q2 False False = False
+  q2 _     _     = True 
 Solution #20:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
   q2 False False = False
   q2 _     _     = True 
 Solution #21:
   q1 :: Bool -> Bool
-  q1 _ = True
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True  = True 
   q2 True  False = True 
+  q2 False True  = True 
   q2 _     _     = False
 Solution #22:
   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 True = True 
+  q2 _     _    = False
 Solution #23:
   q1 :: Bool -> Bool
   q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True 
-  q2 _    _     = False
+  q2 False True = True 
+  q2 _     _    = False
 Solution #24:
   q1 :: Bool -> Bool
-  q1 False = True 
-  q1 _     = False
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True  = True 
-  q2 True False = True 
-  q2 _    _     = False
+  q2 False True = True 
+  q2 _     _    = False
 Solution #25:
   q1 :: Bool -> Bool
-  q1 False = True 
-  q1 _     = False
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True 
-  q2 _    _     = False
+  q2 False True = True 
+  q2 True  True = True 
+  q2 _     _    = False
 Solution #26:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 True = True 
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True  = True 
-  q2 True False = True 
-  q2 _    _     = False
+  q2 False True = True 
+  q2 True  True = True 
+  q2 _     _    = False
 Solution #27:
   q1 :: Bool -> Bool
-  q1 True = True 
-  q1 _    = False
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True  = True 
   q2 True False = True 
+  q2 True True  = True 
   q2 _    _     = False
 Solution #28:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 True = True 
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  False = False
+  q2 False True  = False
   q2 False False = False
   q2 _     _     = True 
 Solution #29:
@@ -2107,21 +2106,20 @@ Solution #29:
   q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True 
-  q2 _    _    = False
+  q2 True  True = True 
+  q2 False True = True 
+  q2 _     _    = False
 Solution #30:
   q1 :: Bool -> Bool
   q1 True = True 
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True  = True 
-  q2 True  False = True 
-  q2 _     _     = False
+  q2 True True = True 
+  q2 _    _    = False
 Solution #31:
   q1 :: Bool -> Bool
-  q1 True = True 
-  q1 _    = False
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
   q2 False True = True 
@@ -2131,101 +2129,103 @@ Solution #32:
   q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = False
-  q2 _     _     = True 
+  q2 False True  = True 
+  q2 True  False = True 
+  q2 _     _     = False
 Solution #33:
   q1 :: Bool -> Bool
-  q1 _ = False
+  q1 True = True 
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True 
-  q2 _    _     = False
+  q2 True  True  = False
+  q2 False False = False
+  q2 _     _     = True 
 Solution #34:
   q1 :: Bool -> Bool
   q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False True = True 
-  q2 _     _    = False
+  q2 True False = True 
+  q2 _    _     = False
 Solution #35:
   q1 :: Bool -> Bool
-  q1 True = True 
-  q1 _    = False
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = True 
-  q2 _    _    = False
+  q2 False False = False
+  q2 _     _     = True 
 Solution #36:
   q1 :: Bool -> Bool
   q1 True = True 
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = True 
-  q2 _    _     = False
+  q2 False False = False
+  q2 _     _     = True 
 Solution #37:
   q1 :: Bool -> Bool
   q1 True = True 
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = False
+  q2 False True = True 
+  q2 _     _    = False
 Solution #38:
   q1 :: Bool -> Bool
   q1 True = True 
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True  False = False
-  q2 False False = False
-  q2 _     _     = True 
+  q2 True False = True 
+  q2 _    _     = False
 Solution #39:
   q1 :: Bool -> Bool
   q1 True = True 
   q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = False
-  q2 _     _     = True 
+  q2 _ _ = False
 Solution #40:
   q1 :: Bool -> Bool
-  q1 True = True 
-  q1 _    = False
+  q1 _ = True
 
   q2 :: Bool -> Bool -> Bool
-  q2 True False = False
-  q2 True True  = False
-  q2 _    _     = True 
+  q2 True  False = True 
+  q2 False False = True 
+  q2 _     _     = False
 Solution #41:
   q1 :: Bool -> Bool
-  q1 True = True 
-  q1 _    = False
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True 
+  q2 True  False = True 
+  q2 False False = True 
+  q2 _     _     = False
 Solution #42:
   q1 :: Bool -> Bool
-  q1 True = True 
-  q1 _    = False
+  q1 True = False
+  q1 _    = True 
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = True
+  q2 False False = True 
+  q2 _     _     = False
 Solution #43:
   q1 :: Bool -> Bool
-  q1 False = True 
-  q1 _     = False
+  q1 _ = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 _ _ = True
+  q2 True False = False
+  q2 True True  = False
+  q2 _    _     = True 
 Solution #44:
   q1 :: Bool -> Bool
-  q1 False = True 
-  q1 _     = False
+  q1 True = True 
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 True True = False
-  q2 _    _    = True 
+  q2 _ _ = True
 Solution #45:
   q1 :: Bool -> Bool
   q1 _ = False
@@ -2235,21 +2235,21 @@ Solution #45:
   q2 _    _    = True 
 Solution #46:
   q1 :: Bool -> Bool
-  q1 False = True 
-  q1 _     = False
+  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 #47:
   q1 :: Bool -> Bool
-  q1 True = False
-  q1 _    = True 
+  q1 True = True 
+  q1 _    = False
 
   q2 :: Bool -> Bool -> Bool
-  q2 False False = True 
-  q2 _     _     = False
+  q2 True False = False
+  q2 True True  = False
+  q2 _    _     = True 
 Solution #48:
   q1 :: Bool -> Bool
   q1 _ = False
diff --git a/SBVTestSuite/GoldFiles/validate_2.gold b/SBVTestSuite/GoldFiles/validate_2.gold
index 75827f02f..80d0de7d2 100644
--- a/SBVTestSuite/GoldFiles/validate_2.gold
+++ b/SBVTestSuite/GoldFiles/validate_2.gold
@@ -29,11 +29,11 @@
 [SEND] (check-sat)
 [RECV] sat
 [SEND] (get-value (s0))
-[RECV] ((s0 (fp #b0 #x00 #b11111111111111111011000)))
+[RECV] ((s0 (_ +zero 8 24)))
 *** Solver   : Z3
 *** Exit code: ExitSuccess
 [VALIDATE] Validating the model. Assignment:
-[VALIDATE]       x = 1.1754887e-38 :: Float
+[VALIDATE]       x = 0.0 :: Float
 [VALIDATE] There are no constraints to check.
 [VALIDATE] Validating outputs.
 
@@ -42,7 +42,7 @@ FINAL OUTPUT:
 *** 
 *** Assignment:
 *** 
-***       x = 1.1754887e-38 :: Float
+***       x = 0.0 :: Float
 *** 
 *** Floating point FMA operation is not supported concretely.
 *** 
@@ -52,4 +52,4 @@ FINAL OUTPUT:
 *** Alleged model:
 ***
 *** Satisfiable. Model:
-***   x = 1.1754887e-38 :: Float
+***   x = 0.0 :: Float
diff --git a/SMTSolverVersions.md b/SMTSolverVersions.md
index d556a24cd..98500996b 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 Nov 29th, 2023
+      * Version as downloaded from the above site on Dec 4th, 2023
       * 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.