New example

[LeventErkok]

Turn this into an example, taken from https://hugopeters.me/posts/15/

{-# OPTIONS_GHC -Wall -Werror #-}

import Data.SBV
import Data.SBV.Either

main :: IO ()
main = print =<< allSatWith z3{isNonModelVar = (== "jIsInt")} puzzle

puzzle :: Symbolic ()
puzzle = do
    a <- sInteger "a"
    b <- sInteger "b"
    c <- sBool    "c"
    d <- sInteger "d"
    e <- sBool    "e"
    f <- sInteger "f"
    g <- sBool    "g"
    h <- sInteger "h"
    i <- sBool    "i"
    j <- sEither  "j"

    jIsInt <- sBool "jIsInt"

    let ints  intj = [a, b, d, f, h] ++ [fromRight j |     intj]
        bools intj = [c, e, g, i]    ++ [fromLeft  j | not intj]

        choice fn = ite jIsInt (fn True) (fn False)

    -- a. What is sum of all integer answers?
    constrain $ a .== choice (sum . ints)

    -- b. How many boolean answers are true?
    constrain $ b .== choice (sum . map oneIf . bools)

    -- c. Is a the largest number?
    constrain $ c .== (a .== choice (foldr1 smax . ints))

    -- d. How many integers are equal to me?
    constrain $ d .== choice (sum . map (oneIf . (d .==)) . ints)

    -- e. Are all integers positive?
    constrain $ e .== choice (sAll (.> 0) . ints)

    -- f. What is the average of all integers?
    constrain $ f * choice (literal . toInteger . length . ints) .== choice (sum . ints)

    -- g. is d strictly larger than b?
    constrain $ g .== (d .> b)

    -- h. what is a / h?
    constrain $ h * h .== a

    -- i. is f equal to d - b - h * d?
    constrain $ i .== (f .== d - b - h * d)

    -- j. what is the answer to this question?
    constrain $ ite jIsInt (isRight j) (isLeft j)

Prints:

Solution #1:
  a =         144 :: Integer
  b =           2 :: Integer
  c =        True :: Bool
  d =           2 :: Integer
  e =       False :: Bool
  f =          24 :: Integer
  g =       False :: Bool
  h =         -12 :: Integer
  i =        True :: Bool
  j = Right (-16) :: Either Bool Integer
This is the only solution.