diff --git a/Data/SBV.hs b/Data/SBV.hs
--- a/Data/SBV.hs
+++ b/Data/SBV.hs
@@ -133,7 +133,7 @@
   -- ** Symbolic numbers
   , SNum
   -- ** Division
-  , BVDivisible(..)
+  , SDivisible(..)
   -- ** The Boolean class
   , Boolean(..)
   -- *** Generalizations of boolean operations
@@ -387,7 +387,7 @@
 
    * Extraction and concatenation: 'split', '#', and 'extend' (see the 'Splittable' class)
 
-Usual arithmetic ('+', '-', '*', 'bvQuotRem') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are
+Usual arithmetic ('+', '-', '*', 'sQuotRem', 'sQuot', 'sRem', 'sDivMod', 'sDiv', 'sMod') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are
 supported for 'SInteger' fully, both in programming and verification modes.
 -}
 
diff --git a/Data/SBV/BitVectors/AlgReals.hs b/Data/SBV/BitVectors/AlgReals.hs
--- a/Data/SBV/BitVectors/AlgReals.hs
+++ b/Data/SBV/BitVectors/AlgReals.hs
@@ -13,12 +13,13 @@
 {-# LANGUAGE TypeSynonymInstances #-}
 {-# OPTIONS_GHC -fno-warn-orphans #-}
 
-module Data.SBV.BitVectors.AlgReals (AlgReal(..), mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals) where
+module Data.SBV.BitVectors.AlgReals (AlgReal(..), mkPolyReal, algRealToSMTLib2, algRealToHaskell, mergeAlgReals, isExactRational, algRealStructuralEqual, algRealStructuralCompare) where
 
-import Data.List     (sortBy, isPrefixOf, partition)
-import Data.Ratio    ((%), numerator, denominator)
-import Data.Function (on)
+import Data.List       (sortBy, isPrefixOf, partition)
+import Data.Ratio      ((%), numerator, denominator)
+import Data.Function   (on)
 import System.Random
+import Test.QuickCheck (Arbitrary(..))
 
 -- | Algebraic reals. Note that the representation is left abstract. We represent
 -- rational results explicitly, while the roots-of-polynomials are represented
@@ -27,10 +28,16 @@
              | AlgPolyRoot (Integer,  Polynomial) -- which root
                            (Maybe String)         -- approximate decimal representation with given precision, if available
 
+-- | Check wheter a given argument is an exact rational
+isExactRational :: AlgReal -> Bool
+isExactRational (AlgRational True _) = True
+isExactRational _                    = False
+
 -- | A univariate polynomial, represented simply as a
 -- coefficient list. For instance, "5x^3 + 2x - 5" is
 -- represented as [(5, 3), (2, 1), (-5, 0)]
 newtype Polynomial = Polynomial [(Integer, Integer)]
+                   deriving (Eq, Ord)
 
 -- | Construct a poly-root real with a given approximate value (either as a decimal, or polynomial-root)
 mkPolyReal :: Either (Bool, String) (Integer, [(Integer, Integer)]) -> AlgReal
@@ -96,6 +103,18 @@
   AlgRational True a `compare` AlgRational True b = a `compare` b
   a                  `compare` b                  = error $ "AlgReal.compare: unsupported arguments: " ++ show (a, b)
 
+-- Structural equality and ord for AlgReal; used when constants are Map keys
+algRealStructuralEqual   :: AlgReal -> AlgReal -> Bool
+AlgRational a b `algRealStructuralEqual` AlgRational c d = (a, b) == (c, d)
+AlgPolyRoot a b `algRealStructuralEqual` AlgPolyRoot c d = (a, b) == (c, d)
+_               `algRealStructuralEqual` _               = False
+
+algRealStructuralCompare :: AlgReal -> AlgReal -> Ordering
+AlgRational a b `algRealStructuralCompare` AlgRational c d = (a, b) `compare` (c, d)
+AlgRational _ _ `algRealStructuralCompare` AlgPolyRoot _ _ = LT
+AlgPolyRoot _ _ `algRealStructuralCompare` AlgRational _ _ = GT
+AlgPolyRoot a b `algRealStructuralCompare` AlgPolyRoot c d = (a, b) `compare` (c, d)
+
 instance Num AlgReal where
   (+)         = lift2 "+"      (+)
   (*)         = lift2 "*"      (*)
@@ -198,3 +217,7 @@
   | e1                   = f
   | e2                   = s
 mergeAlgReals m _ _ = error m
+
+-- Quickcheck instance
+instance Arbitrary AlgReal where
+  arbitrary = AlgRational True `fmap` arbitrary
diff --git a/Data/SBV/BitVectors/Data.hs b/Data/SBV/BitVectors/Data.hs
--- a/Data/SBV/BitVectors/Data.hs
+++ b/Data/SBV/BitVectors/Data.hs
@@ -64,8 +64,29 @@
 data CWVal = CWAlgReal       AlgReal    -- ^ algebraic real
            | CWInteger       Integer    -- ^ bit-vector/unbounded integer
            | CWUninterpreted String     -- ^ value of an uninterpreted kind
-           deriving (Eq, Ord)
 
+-- We cannot simply derive Eq/Ord for CWVal, since CWAlgReal doesn't have proper
+-- instances for these when values are infinitely precise reals. However, we do
+-- need a structural eq/ord for Map indexes; so define custom ones here:
+instance Eq CWVal where
+  CWAlgReal a       == CWAlgReal b       = a `algRealStructuralEqual` b
+  CWInteger a       == CWInteger b       = a == b
+  CWUninterpreted a == CWUninterpreted b = a == b
+  _                 == _                 = False
+
+instance Ord CWVal where
+  CWAlgReal a       `compare` CWAlgReal b       = a `algRealStructuralCompare` b
+  CWAlgReal _       `compare` CWInteger _       = LT
+  CWAlgReal _       `compare` CWUninterpreted _ = LT
+
+  CWInteger _       `compare` CWAlgReal _       = GT
+  CWInteger a       `compare` CWInteger b       = a `compare` b
+  CWInteger _       `compare` CWUninterpreted _ = LT
+
+  CWUninterpreted _ `compare` CWAlgReal _       = GT
+  CWUninterpreted _ `compare` CWInteger _       = GT
+  CWUninterpreted a `compare` CWUninterpreted b = a `compare` b
+
 -- | 'CW' represents a concrete word of a fixed size:
 -- Endianness is mostly irrelevant (see the 'FromBits' class).
 -- For signed words, the most significant digit is considered to be the sign.
@@ -163,7 +184,7 @@
 
 -- | Symbolic operations
 data Op = Plus | Times | Minus
-        | Quot | Rem -- quot and rem are unsigned only
+        | Quot | Rem
         | Equal | NotEqual
         | LessThan | GreaterThan | LessEq | GreaterEq
         | Ite
diff --git a/Data/SBV/BitVectors/Model.hs b/Data/SBV/BitVectors/Model.hs
--- a/Data/SBV/BitVectors/Model.hs
+++ b/Data/SBV/BitVectors/Model.hs
@@ -14,6 +14,7 @@
 {-# LANGUAGE TypeSynonymInstances   #-}
 {-# LANGUAGE BangPatterns           #-}
 {-# LANGUAGE PatternGuards          #-}
+{-# LANGUAGE FlexibleContexts       #-}
 {-# LANGUAGE FlexibleInstances      #-}
 {-# LANGUAGE MultiParamTypeClasses  #-}
 {-# LANGUAGE ScopedTypeVariables    #-}
@@ -21,7 +22,7 @@
 {-# LANGUAGE Rank2Types             #-}
 
 module Data.SBV.BitVectors.Model (
-    Mergeable(..), EqSymbolic(..), OrdSymbolic(..), BVDivisible(..), Uninterpreted(..), SNum
+    Mergeable(..), EqSymbolic(..), OrdSymbolic(..), SDivisible(..), Uninterpreted(..), SNum
   , sbvTestBit, sbvPopCount, setBitTo, allEqual, allDifferent, oneIf, blastBE, blastLE
   , lsb, msb, genVar, genVar_, forall, forall_, exists, exists_
   , constrain, pConstrain, sBool, sBools, sWord8, sWord8s, sWord16, sWord16s, sWord32
@@ -60,16 +61,16 @@
    where c st = do swa <- sbvToSW st a
                    opS st k swa
 
-liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b
-liftSym2 _   opCR opCI   (SBV k (Left a)) (SBV _ (Left b)) = SBV k $ Left  $ mapCW2 opCR opCI noUnint2 a b
-liftSym2 opS _    _    a@(SBV k _)        b                = SBV k $ Right $ cache c
+liftSym2 :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> AlgReal) -> (Integer -> Integer -> Integer) -> SBV b -> SBV b -> SBV b
+liftSym2 _   okCW opCR opCI   (SBV k (Left a)) (SBV _ (Left b)) | okCW a b = SBV k $ Left  $ mapCW2 opCR opCI noUnint2 a b
+liftSym2 opS _    _    _    a@(SBV k _)        b                           = SBV k $ Right $ cache c
   where c st = do sw1 <- sbvToSW st a
                   sw2 <- sbvToSW st b
                   opS st k sw1 sw2
 
-liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool
-liftSym2B _   opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) = literal (liftCW2 opCR opCI noUnint2 a b)
-liftSym2B opS _    _    a                b                = SBV (KBounded False 1) $ Right $ cache c
+liftSym2B :: (State -> Kind -> SW -> SW -> IO SW) -> (CW -> CW -> Bool) -> (AlgReal -> AlgReal -> Bool) -> (Integer -> Integer -> Bool) -> SBV b -> SBV b -> SBool
+liftSym2B _   okCW opCR opCI (SBV _ (Left a)) (SBV _ (Left b)) | okCW a b = literal (liftCW2 opCR opCI noUnint2 a b)
+liftSym2B opS _    _    _    a                b                           = SBV (KBounded False 1) $ Right $ cache c
   where c st = do sw1 <- sbvToSW st a
                   sw2 <- sbvToSW st b
                   opS st (KBounded False 1) sw1 sw2
@@ -199,6 +200,11 @@
   literal    = SBV KReal . Left . CW KReal . CWAlgReal
   fromCW (CW _ (CWAlgReal a)) = a
   fromCW c                    = error $ "SymWord.AlgReal: Unexpected non-real value: " ++ show c
+  -- AlgReal needs its own definition of isConcretely
+  -- to make sure we avoid using unimplementable Haskell functions
+  isConcretely (SBV KReal (Left (CW KReal (CWAlgReal v)))) p
+     | isExactRational v = p v
+  isConcretely _ _       = False
   mbMaxBound = Nothing
   mbMinBound = Nothing
 
@@ -343,8 +349,8 @@
 -}
 
 instance EqSymbolic (SBV a) where
-  (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW)  Equal)    (==) (==)
-  (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) (/=) (/=)
+  (.==) = liftSym2B (mkSymOpSC (eqOpt trueSW)  Equal)    rationalCheck (==) (==)
+  (./=) = liftSym2B (mkSymOpSC (eqOpt falseSW) NotEqual) rationalCheck (/=) (/=)
 
 eqOpt :: SW -> SW -> SW -> Maybe SW
 eqOpt w x y = if x == y then Just w else Nothing
@@ -353,19 +359,19 @@
   x .< y
     | Just mb <- mbMaxBound, x `isConcretely` (== mb) = false
     | Just mb <- mbMinBound, y `isConcretely` (== mb) = false
-    | True                                            = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan)    (<)  (<)  x y
+    | True                                            = liftSym2B (mkSymOpSC (eqOpt falseSW) LessThan)    rationalCheck (<)  (<)  x y
   x .<= y
     | Just mb <- mbMinBound, x `isConcretely` (== mb) = true
     | Just mb <- mbMaxBound, y `isConcretely` (== mb) = true
-    | True                                            = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq)       (<=) (<=) x y
+    | True                                            = liftSym2B (mkSymOpSC (eqOpt trueSW) LessEq)       rationalCheck (<=) (<=) x y
   x .> y
     | Just mb <- mbMinBound, x `isConcretely` (== mb) = false
     | Just mb <- mbMaxBound, y `isConcretely` (== mb) = false
-    | True                                            = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) (>)  (>)  x y
+    | True                                            = liftSym2B (mkSymOpSC (eqOpt falseSW) GreaterThan) rationalCheck (>)  (>)  x y
   x .>= y
     | Just mb <- mbMaxBound, x `isConcretely` (== mb) = true
     | Just mb <- mbMinBound, y `isConcretely` (== mb) = true
-    | True                                            = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq)    (>=) (>=) x y
+    | True                                            = liftSym2B (mkSymOpSC (eqOpt trueSW) GreaterEq)    rationalCheck (>=) (>=) x y
 
 -- Bool
 instance EqSymbolic Bool where
@@ -536,16 +542,16 @@
   x + y
     | x `isConcretely` (== 0) = y
     | y `isConcretely` (== 0) = x
-    | True                    = liftSym2 (mkSymOp Plus)  (+) (+) x y
+    | True                    = liftSym2 (mkSymOp Plus)  rationalCheck (+) (+) x y
   x * y
     | x `isConcretely` (== 0) = 0
     | y `isConcretely` (== 0) = 0
     | x `isConcretely` (== 1) = y
     | y `isConcretely` (== 1) = x
-    | True                    = liftSym2 (mkSymOp Times) (*) (*) x y
+    | True                    = liftSym2 (mkSymOp Times) rationalCheck (*) (*) x y
   x - y
     | y `isConcretely` (== 0) = x
-    | True                    = liftSym2 (mkSymOp Minus) (-) (-) x y
+    | True                    = liftSym2 (mkSymOp Minus) rationalCheck (-) (-) x y
   abs a
    | hasSign a = ite (a .< 0) (-a) a
    | True      = a
@@ -555,10 +561,21 @@
 
 instance Fractional SReal where
   fromRational = literal . fromRational
-  x / y        = liftSym2 (mkSymOp Quot) (/) die x y
+  x / y        = liftSym2 (mkSymOp Quot) rationalCheck (/) die x y
    where -- should never happen
          die = error $ "impossible: non-real value found in Fractional.SReal " ++ show (x, y)
 
+-- Most operations on concrete rationals require a compatibility check
+rationalCheck :: CW -> CW -> Bool
+rationalCheck a b = case (cwVal a, cwVal b) of
+                     (CWAlgReal x, CWAlgReal y) -> isExactRational x && isExactRational y
+                     _                          -> True
+
+-- same as above, for SBV's
+rationalSBVCheck :: SBV a -> SBV a -> Bool
+rationalSBVCheck (SBV KReal (Left a)) (SBV KReal (Left b)) = rationalCheck a b
+rationalSBVCheck _                    _                    = True
+
 -- Some operations will never be used on Reals, but we need fillers:
 noReal :: String -> AlgReal -> AlgReal -> AlgReal
 noReal o a b = error $ "SBV.AlgReal." ++ o ++ ": Unexpected arguments: " ++ show (a, b)
@@ -574,17 +591,17 @@
     | x `isConcretely` (== -1) = y
     | y `isConcretely` (== 0)  = 0
     | y `isConcretely` (== -1) = x
-    | True                     = liftSym2 (mkSymOp  And) (noReal ".&.") (.&.) x y
+    | True                     = liftSym2 (mkSymOp  And) (const (const True)) (noReal ".&.") (.&.) x y
   x .|. y
     | x `isConcretely` (== 0)  = y
     | x `isConcretely` (== -1) = -1
     | y `isConcretely` (== 0)  = x
     | y `isConcretely` (== -1) = -1
-    | True                     = liftSym2 (mkSymOp  Or)  (noReal ".|.") (.|.) x y
+    | True                     = liftSym2 (mkSymOp  Or)  (const (const True)) (noReal ".|.") (.|.) x y
   x `xor` y
     | x `isConcretely` (== 0)  = y
     | y `isConcretely` (== 0)  = x
-    | True                     = liftSym2 (mkSymOp  XOr) (noReal "xor") xor x y
+    | True                     = liftSym2 (mkSymOp  XOr) (const (const True)) (noReal "xor") xor x y
   complement = liftSym1 (mkSymOp1 Not) (noRealUnary "Not") complement
   bitSize  _ = intSizeOf (undefined :: a)
   isSigned _ = hasSign   (undefined :: a)
@@ -731,100 +748,160 @@
                 Nothing -> error $ "Enum." ++ w ++ "{" ++ showType x ++ "}: Called on symbolic value " ++ show x
                 Just v  -> fromIntegral v
 
--- | The 'BVDivisible' class captures the essence of division of words.
+-- | The 'SDivisible' class captures the essence of division.
 -- Unfortunately we cannot use Haskell's 'Integral' class since the 'Real'
 -- and 'Enum' superclasses are not implementable for symbolic bit-vectors.
--- However, 'quotRem' makes perfect sense, and the 'BVDivisible' class captures
+-- However, 'quotRem' and 'divMod' makes perfect sense, and the 'SDivisible' class captures
 -- this operation. One issue is how division by 0 behaves. The verification
 -- technology requires total functions, and there are several design choices
 -- here. We follow Isabelle/HOL approach of assigning the value 0 for division
 -- by 0. Therefore, we impose the following law:
 --
---     @ x `bvQuotRem` 0 = (0, x) @
+--     @ x `sQuotRem` 0 = (0, x) @
+--     @ x `sDivMod`  0 = (0, x) @
 --
 -- Note that our instances implement this law even when @x@ is @0@ itself.
 --
--- Minimal complete definition: 'bvQuotRem'
-class BVDivisible a where
-  bvQuotRem :: a -> a -> (a, a)
+-- NB. 'quot' truncates toward zero, while 'div' truncates toward negative infinity.
+--
+-- Minimal complete definition: 'sQuotRem', 'sDivMod'
+class SDivisible a where
+  sQuotRem :: a -> a -> (a, a)
+  sDivMod  :: a -> a -> (a, a)
+  sQuot    :: a -> a -> a
+  sRem     :: a -> a -> a
+  sDiv     :: a -> a -> a
+  sMod     :: a -> a -> a
 
-instance BVDivisible Word64 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+  x `sQuot` y = fst $ x `sQuotRem` y
+  x `sRem`  y = snd $ x `sQuotRem` y
+  x `sDiv`  y = fst $ x `sDivMod`  y
+  x `sMod`  y = snd $ x `sDivMod`  y
 
-instance BVDivisible Int64 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Word64 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Word32 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Int64 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Int32 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Word32 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Word16 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Int32 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Int16 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Word16 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Word8 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Int16 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Int8 where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Word8 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible Integer where
-  bvQuotRem x 0 = (0, x)
-  bvQuotRem x y = x `quotRem` y
+instance SDivisible Int8 where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible CW where
-  bvQuotRem a b
-    | CWInteger x <- cwVal a, CWInteger y <- cwVal b
-    = let (r1, r2) = bvQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })
-  bvQuotRem a b = error $ "SBV.liftQRem: impossible, unexpected args received: " ++ show (a, b)
+instance SDivisible Integer where
+  sQuotRem x 0 = (0, x)
+  sQuotRem x y = x `quotRem` y
+  sDivMod  x 0 = (0, x)
+  sDivMod  x y = x `divMod` y
 
-instance BVDivisible SWord64 where
-  bvQuotRem = liftQRem
+instance SDivisible CW where
+  sQuotRem a b
+    | CWInteger x <- cwVal a, CWInteger y <- cwVal b
+    = let (r1, r2) = sQuotRem x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })
+  sQuotRem a b = error $ "SBV.sQuotRem: impossible, unexpected args received: " ++ show (a, b)
+  sDivMod a b
+    | CWInteger x <- cwVal a, CWInteger y <- cwVal b
+    = let (r1, r2) = sDivMod x y in (a { cwVal = CWInteger r1 }, b { cwVal = CWInteger r2 })
+  sDivMod a b = error $ "SBV.sDivMod: impossible, unexpected args received: " ++ show (a, b)
 
-instance BVDivisible SInt64 where
-  bvQuotRem = liftQRem
+instance SDivisible SWord64 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SWord32 where
-  bvQuotRem = liftQRem
+instance SDivisible SInt64 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SInt32 where
-  bvQuotRem = liftQRem
+instance SDivisible SWord32 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SWord16 where
-  bvQuotRem = liftQRem
+instance SDivisible SInt32 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SInt16 where
-  bvQuotRem = liftQRem
+instance SDivisible SWord16 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SWord8 where
-  bvQuotRem = liftQRem
+instance SDivisible SInt16 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SInt8 where
-  bvQuotRem = liftQRem
+instance SDivisible SWord8 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-instance BVDivisible SInteger where
-  bvQuotRem = liftQRem
+instance SDivisible SInt8 where
+  sQuotRem = liftQRem
+  sDivMod  = liftDMod
 
-liftQRem :: (SymWord a, Num a, BVDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)
+liftQRem :: (SymWord a, Num a, SDivisible a) => SBV a -> SBV a -> (SBV a, SBV a)
 liftQRem x y = ite (y .== 0) (0, x) (qr x y)
-  where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = bvQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r))
+  where qr (SBV sgnsz (Left a)) (SBV _ (Left b)) = let (q, r) = sQuotRem a b in (SBV sgnsz (Left q), SBV sgnsz (Left r))
         qr a@(SBV sgnsz _)      b                = (SBV sgnsz (Right (cache (mk Quot))), SBV sgnsz (Right (cache (mk Rem))))
                 where mk o st = do sw1 <- sbvToSW st a
                                    sw2 <- sbvToSW st b
                                    mkSymOp o st sgnsz sw1 sw2
 
+-- Conversion from quotRem (truncate to 0) to divMod (truncate towards negative infinity)
+liftDMod :: (SymWord a, Num a, SDivisible a, SDivisible (SBV a)) => SBV a -> SBV a -> (SBV a, SBV a)
+liftDMod x y = ite (y .== 0) (0, x) $ ite (signum r .== negate (signum y)) (q-1, r+y) qr
+   where qr@(q, r) = x `sQuotRem` y
+
+-- SInteger instance for quotRem/divMod are tricky!
+-- SMT-Lib only has Euclidean operations, but Haskell
+-- uses "truncate to 0" for quotRem, and "truncate to negative infinity" for divMod.
+-- So, we cannot just use the above liftings directly.
+instance SDivisible SInteger where
+  sDivMod = liftDMod
+  sQuotRem x y
+    | not (isSymbolic x || isSymbolic y)
+    = liftQRem x y
+    | True
+    = ite (y .== 0) (0, x) (qE+i, rE-i*y)
+    where (qE, rE) = liftQRem x y   -- for integers, this is euclidean due to SMTLib semantics
+          i = ite (x .>= 0 ||| rE .== 0) 0
+            $ ite (y .>  0)              1 (-1)
+
 -- Quickcheck interface
 
 -- The Arbitrary instance for SFunArray returns an array initialized
@@ -890,7 +967,7 @@
   -- Of course, we do not have a way of enforcing that in the user code, but
   -- at least our library code respects that invariant.
   symbolicMerge t a@(SBV{}) b@(SBV{})
-     | Just av <- unliteral a, Just bv <- unliteral b, av == bv
+     | Just av <- unliteral a, Just bv <- unliteral b, rationalSBVCheck a b, av == bv
      = a
      | True
      = SBV k $ Right $ cache c
diff --git a/Data/SBV/Compilers/C.hs b/Data/SBV/Compilers/C.hs
--- a/Data/SBV/Compilers/C.hs
+++ b/Data/SBV/Compilers/C.hs
@@ -507,6 +507,8 @@
                                                                      Just i  -> (True, canOverflow True i)
                                                KUninterpreted s -> die $ "Uninterpreted sort: " ++ s
         -- Div/Rem should be careful on 0, in the SBV world x `div` 0 is 0, x `rem` 0 is x
+        -- NB: Quot is supposed to truncate toward 0; Not clear to me if C guarantees this behavior.
+        -- Brief googling suggests C99 does indeed truncate toward 0, but other C compilers might differ.
         p Quot [a, b] = parens (b <+> text "== 0") <+> text "?" <+> text "0" <+> text ":" <+> parens (a <+> text "/" <+> b)
         p Rem  [a, b] = parens (b <+> text "== 0") <+> text "?" <+>    a     <+> text ":" <+> parens (a <+> text "%" <+> b)
         p o [a, b]
diff --git a/Data/SBV/Examples/CodeGeneration/GCD.hs b/Data/SBV/Examples/CodeGeneration/GCD.hs
--- a/Data/SBV/Examples/CodeGeneration/GCD.hs
+++ b/Data/SBV/Examples/CodeGeneration/GCD.hs
@@ -35,7 +35,7 @@
         go x y c = ite (c .== 0 ||| y .== 0)   -- stop if y is 0, or if we reach the recursion depth
                        x
                        (go y y' (c-1))
-          where (_, y') = x `bvQuotRem` y
+          where (_, y') = x `sQuotRem` y
 
 -----------------------------------------------------------------------------
 -- * Verification
@@ -58,8 +58,8 @@
                           (isCommonDivisor k ==> k' .>= k)) -- if k is a common divisor as well, then k' is at least as large as k
   where k' = sgcd x y
         isCommonDivisor a = z1 .== 0 &&& z2 .== 0
-           where (_, z1) = x `bvQuotRem` a
-                 (_, z2) = y `bvQuotRem` a
+           where (_, z1) = x `sQuotRem` a
+                 (_, z2) = y `sQuotRem` a
 
 -----------------------------------------------------------------------------
 -- * Code generation
diff --git a/Data/SBV/Examples/Crypto/AES.hs b/Data/SBV/Examples/Crypto/AES.hs
--- a/Data/SBV/Examples/Crypto/AES.hs
+++ b/Data/SBV/Examples/Crypto/AES.hs
@@ -40,7 +40,7 @@
 type GF28 = SWord8
 
 -- | Multiplication in GF(2^8). This is simple polynomial multipliation, followed
--- by the irreducible polynomial @x^8+x^5+x^3+x^1+1@. We simply use the 'pMult'
+-- by the irreducible polynomial @x^8+x^4+x^3+x^1+1@. We simply use the 'pMult'
 -- function exported by SBV to do the operation. 
 gf28Mult :: GF28 -> GF28 -> GF28
 gf28Mult x y = pMult (x, y, [8, 4, 3, 1, 0])
diff --git a/Data/SBV/Examples/Puzzles/Counts.hs b/Data/SBV/Examples/Puzzles/Counts.hs
--- a/Data/SBV/Examples/Puzzles/Counts.hs
+++ b/Data/SBV/Examples/Puzzles/Counts.hs
@@ -39,8 +39,8 @@
                    (ite (n .< 100)
                         (upd d1 (upd d2 cnts))            -- two digits
                         (upd d1 (upd d2 (upd d3 cnts))))  -- three digits
-  where (r1, d1)   = n  `bvQuotRem` 10
-        (d3, d2)   = r1 `bvQuotRem` 10
+  where (r1, d1)   = n  `sQuotRem` 10
+        (d3, d2)   = r1 `sQuotRem` 10
         upd d = zipWith inc [0..]
           where inc i c = ite (i .== d) (c+1) c
 
diff --git a/Data/SBV/Provers/Prover.hs b/Data/SBV/Provers/Prover.hs
--- a/Data/SBV/Provers/Prover.hs
+++ b/Data/SBV/Provers/Prover.hs
@@ -53,7 +53,17 @@
 import Data.SBV.Utils.Boolean
 
 mkConfig :: SMTSolver -> Bool -> [String] -> SMTConfig
-mkConfig s isSMTLib2 tweaks = SMTConfig {verbose = False, timing = False, timeOut = Nothing, printBase = 10, printRealPrec = 16, smtFile = Nothing, solver = s, solverTweaks = tweaks, useSMTLib2 = isSMTLib2}
+mkConfig s isSMTLib2 tweaks = SMTConfig { verbose = False
+                                        , timing        = False
+                                        , timeOut       = Nothing
+                                        , printBase     = 10
+                                        , printRealPrec = 16
+                                        , smtFile       = Nothing
+                                        , solver        = s
+                                        , solverTweaks  = tweaks
+                                        , useSMTLib2    = isSMTLib2
+                                        , satCmd        = "(check-sat)"
+                                        }
 
 -- | Default configuration for the Yices SMT Solver.
 yices :: SMTConfig
@@ -61,7 +71,7 @@
 
 -- | Default configuration for the Z3 SMT solver
 z3 :: SMTConfig
-z3 = mkConfig Z3.z3 True ["(set-option :mbqi true) ; use model based quantification"]
+z3 = mkConfig Z3.z3 True ["(set-option :mbqi true) ; use model based quantifier instantiation"]
 
 -- | The default solver used by SBV. This is currently set to z3.
 defaultSMTCfg :: SMTConfig
diff --git a/Data/SBV/SMT/SMT.hs b/Data/SBV/SMT/SMT.hs
--- a/Data/SBV/SMT/SMT.hs
+++ b/Data/SBV/SMT/SMT.hs
@@ -53,6 +53,7 @@
        , printBase     :: Int            -- ^ Print integral literals in this base (2, 8, and 10, and 16 are supported.)
        , printRealPrec :: Int            -- ^ Print algebraic real values with this precision. (SReal, default: 16)
        , solverTweaks  :: [String]       -- ^ Additional lines of script to give to the solver (user specified)
+       , satCmd        :: String         -- ^ Usually "(check-sat)". However, users might tweak it based on solver characteristics.
        , smtFile       :: Maybe FilePath -- ^ If Just, the generated SMT script will be put in this file (for debugging purposes mostly)
        , useSMTLib2    :: Bool           -- ^ If True, we'll treat the solver as using SMTLib2 input format. Otherwise, SMTLib1
        , solver        :: SMTSolver      -- ^ The actual SMT solver.
@@ -349,13 +350,13 @@
   where shC s = "       " ++ s
 
 -- | Helper function to spin off to an SMT solver.
-pipeProcess :: Bool -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])
-pipeProcess verb nm execName opts script cleanErrs = do
+pipeProcess :: SMTConfig -> String -> String -> [String] -> SMTScript -> (String -> String) -> IO (Either String [String])
+pipeProcess cfg nm execName opts script cleanErrs = do
         mbExecPath <- findExecutable execName
         case mbExecPath of
           Nothing -> return $ Left $ "Unable to locate executable for " ++ nm
                                    ++ "\nExecutable specified: " ++ show execName
-          Just execPath -> do (ec, contents, allErrors) <- runSolver verb execPath opts script
+          Just execPath -> do (ec, contents, allErrors) <- runSolver cfg execPath opts script
                               let errors = dropWhile isSpace (cleanErrs allErrors)
                               case ec of
                                 ExitSuccess  ->  if null errors
@@ -393,7 +394,7 @@
       Nothing -> return ()
       Just f  -> do putStrLn $ "** Saving the generated script in file: " ++ show f
                     writeFile f (scriptBody script)
-    contents <- timeIf isTiming nmSolver $ pipeProcess (verbose config) nmSolver exec opts script cleanErrs
+    contents <- timeIf isTiming nmSolver $ pipeProcess config nmSolver exec opts script cleanErrs
     msg $ nmSolver ++ " output:\n" ++ either id (intercalate "\n") contents
     case contents of
       Left e   -> return $ failure (lines e)
@@ -401,8 +402,8 @@
 
 -- | A variant of 'readProcessWithExitCode'; except it knows about continuation strings
 -- and can speak SMT-Lib2 (just a little).
-runSolver :: Bool -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)
-runSolver verb execPath opts script
+runSolver :: SMTConfig -> FilePath -> [String] -> SMTScript -> IO (ExitCode, String, String)
+runSolver cfg execPath opts script
  | isNothing $ scriptModel script
  = readProcessWithExitCode execPath opts (scriptBody script)
  | True
@@ -429,11 +430,11 @@
                                       else return (ex,          r ++ "\n" ++ out, err)
                 return (send, ask, cleanUp)
       mapM_ send (lines (scriptBody script))
-      r <- ask "(check-sat)"
+      r <- ask $ satCmd cfg
       when (any (`isPrefixOf` r) ["sat", "unknown"]) $ do
         let mls = lines (fromJust (scriptModel script))
-        when verb $ do putStrLn "** Sending the following model extraction commands:"
-                       mapM_ putStrLn mls
+        when (verbose cfg) $ do putStrLn "** Sending the following model extraction commands:"
+                                mapM_ putStrLn mls
         mapM_ send mls
       cleanUp r
 
diff --git a/Data/SBV/Tools/Optimize.hs b/Data/SBV/Tools/Optimize.hs
--- a/Data/SBV/Tools/Optimize.hs
+++ b/Data/SBV/Tools/Optimize.hs
@@ -84,7 +84,8 @@
         msg "Trying to find a satisfying solution."
         m <- satWith cfg $ valid `fmap` mkExistVars n
         case getModel m of
-          Left _ -> return Nothing
+          Left _ -> do msg "No satisfying solutions found."
+                       return Nothing
           Right (True, _)  -> error "SBV: Backend solver reported \"unknown\""
           Right (False, a) -> do msg $ "First solution found: " ++ show a
                                  let c = cost (map literal a)
diff --git a/Data/SBV/Tools/Polynomial.hs b/Data/SBV/Tools/Polynomial.hs
--- a/Data/SBV/Tools/Polynomial.hs
+++ b/Data/SBV/Tools/Polynomial.hs
@@ -27,7 +27,7 @@
 import Data.SBV.Utils.Boolean
 
 -- | Implements polynomial addition, multiplication, division, and modulus operations
--- over GF(2^n).  NB. Similar to 'bvQuotRem', division by @0@ is interpreted as follows:
+-- over GF(2^n).  NB. Similar to 'sQuotRem', division by @0@ is interpreted as follows:
 --
 --     @x `pDivMod` 0 = (0, x)@
 --
diff --git a/LICENSE b/LICENSE
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-SBV: A library for Symbolic Bitvectors
+SBV: SMT Based Verification in Haskell
 
 Copyright (c) 2010-2012, Levent Erkok (erkokl@gmail.com)
 All rights reserved.
diff --git a/README b/README
--- a/README
+++ b/README
@@ -24,9 +24,14 @@
 bit-vectors. Functions for checking satisfiability (`sat` and `allSat`) are also provided.
 In addition, functions using the SBV library can be compiled to C automatically.
 
+Build Status
+============
+SBV uses Travis-CI's automated build infrastructure, making a build for each commit. Current build status:
+[![Build Status](https://secure.travis-ci.org/LeventErkok/sbv.png?branch=master)](http://travis-ci.org/LeventErkok/sbv)
+
 Resources
 =========
-The sbv library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv).
+The SBV library is hosted at [http://github.com/LeventErkok/sbv](http://github.com/LeventErkok/sbv).
 
 The hackage site
 [http://hackage.haskell.org/package/sbv](http://hackage.haskell.org/package/sbv) is the best place
@@ -36,7 +41,7 @@
 
 Overview
 ========
-The Haskell sbv library provides support for dealing with Symbolic Bit Vectors
+The Haskell SBV library provides support for dealing with Symbolic Bit Vectors
 in Haskell. It introduces the types:
 
   - `SBool`: Symbolic Booleans (bits).
@@ -60,9 +65,9 @@
   - proven correct via an external SMT solver (the `prove` function)
   - checked for satisfiability (the `sat`, and `allSat` functions)
   - used in synthesis (the `sat` function with existentials)
-  - optimized with respect to cost functions (the 'optimize', 'maximize', and 'minimize' functions)
+  - optimized with respect to cost functions (the `optimize`, `maximize`, and `minimize` functions)
   - quick-checked
-  - used in concrete test case generation (the 'genTest' function), rendered as values in various
+  - used in concrete test case generation (the `genTest` function), rendered as values in various
     languages, including Haskell and C.
 
 If a predicate is not valid, `prove` will return a counterexample: An 
@@ -75,17 +80,17 @@
 
 Use of SMT solvers
 ==================
-The sbv library uses third-party SMT solvers via the standard SMT-Lib interface: 
-[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/)
+The SBV library uses third-party SMT solvers via the standard SMT-Lib interface
+[http://goedel.cs.uiowa.edu/smtlib/](http://goedel.cs.uiowa.edu/smtlib/).
 
-The SBV library is designed to work with any SMT-Lib compliant SMT-solver, although integration with
-individual solvers require some library work.
-Currently, we fully support 
-the [Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,
-and 
-the [Yices](http://yices.csl.sri.com) SMT solver from SRI.
-Both solvers are available for Windows, Linux, and Mac OSX.
+Currently, we fully support the
+[Z3](http://research.microsoft.com/en-us/um/redmond/projects/z3/) SMT solver from Microsoft,
+and the [Yices](http://yices.csl.sri.com) SMT solver from SRI. Both solvers are available
+for Windows, Linux, and Mac OSX.
 
+Other SMT solvers can be used with SBV as well, with a relatively easy hook-up mechanism. Please
+do get in touch if you plan to use SBV with any other solver.
+
 Prerequisites
 =============
 You **should** have at least one of 
@@ -98,7 +103,7 @@
 of the yices executable in the environment variable `SBV_YICES` and the options to yices in `SBV_YICES_OPTIONS`.
 (The default for the latter is `"-m -f"`). Similarly the environment variables `SBV_Z3` and `SBV_Z3_OPTIONS` can
 be used for choosing executable location and custom options for Z3.  (The default for the latter is
-`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 3.2 or later.)
+`"/in /smt2"` on Windows and `"-in -smt2"` on Mac and Linux. You should use Z3 version 4.1 or later.)
 
 Examples
 =========
@@ -110,7 +115,7 @@
 
 Installation
 ============
-The sbv library is cabalized. Assuming you have cabal/ghc installed, it should merely
+The SBV library is cabalized. Assuming you have cabal/ghc installed, it should merely
 be a matter of running 
      
          cabal install sbv
@@ -118,11 +123,11 @@
 Please see [INSTALL](http://github.com/LeventErkok/sbv/tree/master/INSTALL) for installation details.
 
 Once the installation is done, you can run the executable `SBVUnitTests` which will
-execute the regression test suite for sbv on your machine to ensure all is well.
+execute the regression test suite for SBV on your machine to ensure all is well.
 
 Copyright, License
 ==================
-The sbv library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for
+The SBV library is distributed with the BSD3 license. See [COPYRIGHT](http://github.com/LeventErkok/sbv/tree/master/COPYRIGHT) for
 details. The [LICENSE](http://github.com/LeventErkok/sbv/tree/master/LICENSE) file contains
 the [BSD3](http://en.wikipedia.org/wiki/BSD_licenses) verbiage.
 
diff --git a/RELEASENOTES b/RELEASENOTES
--- a/RELEASENOTES
+++ b/RELEASENOTES
@@ -1,7 +1,29 @@
 Hackage: <http://hackage.haskell.org/package/sbv>
 GitHub:  <http://github.com/LeventErkok/sbv>
 
-Latest Hackage released version: 2.3
+Latest Hackage released version: 2.4
+
+======================================================================
+Version 2.4, 2012-10-19
+
+  - Add missing QuickCheck instance for SReal
+  - When dealing with concrete SReal's, make sure to operate
+    only on exact algebraic reals on the Haskell side, leaving
+    true algebraic reals (i.e., those that are roots of polynomials
+    that cannot be expressed as a rational) symbolic. This avoids
+    issues with functions that we cannot implement directly on
+    the Haskell side, like exact square-roots.
+  - Documentation tweaks, typo fixes etc.
+  - Rename BVDivisible class to SDivisible; since SInteger
+    is also an instance of this class, and SDivisible is a
+    more appropriate name to start with. Also add sQuot and sRem
+    methods; along with sDivMod, sDiv, and sMod, with usual
+    semantics. 
+  - Improve test suite, adding many constant-folding tests
+    and start using cabal based tests (--enable-tests option.)
+  - Stop putting bounds on hackage dependencies, as they cause
+    more trouble then they actually help. (See the discussion
+    here: http://www.haskell.org/pipermail/haskell-cafe/2012-July/102352.html.)
 
 ======================================================================
 Version 2.3, 2012-07-20
diff --git a/SBVUnitTest/Examples/Basics/QRem.hs b/SBVUnitTest/Examples/Basics/QRem.hs
--- a/SBVUnitTest/Examples/Basics/QRem.hs
+++ b/SBVUnitTest/Examples/Basics/QRem.hs
@@ -6,7 +6,7 @@
 -- Maintainer  :  erkokl@gmail.com
 -- Stability   :  experimental
 --
--- Testing the qrem (quote-rem) function
+-- Testing the sQuotRem and sDivMod
 -----------------------------------------------------------------------------
 
 module Examples.Basics.QRem where
@@ -14,12 +14,17 @@
 import Data.SBV
 
 -- check: if (a, b) = x `quotRem` y then x = y*a + b
+-- same is also true for divMod
 -- being careful about y = 0. When divisor is 0, then quotient is
 -- defined to be 0 and the remainder is the numerator
-qrem :: (Num a, EqSymbolic a, BVDivisible a) => a -> a -> SBool
-qrem x y = ite (y .== 0) ((0, x) .== (a, b)) (x .== y * a + b)
-  where (a, b) = x `bvQuotRem` y
+qrem :: (Num a, EqSymbolic a, SDivisible a) => a -> a -> SBool
+qrem x y = ite (y .== 0)
+               ((0, x) .== (q, r) &&& (0, x) .== (d, m))
+               (x .== y * q + r &&& x .== y * d + m)
+  where (q, r) = x `sQuotRem` y
+        (d, m) = x `sDivMod` y
 
 check :: IO ()
-check = print =<< prove (qrem :: SWord8 -> SWord8 -> SBool)
-         -- print =<< prove (qrem :: SWord16 -> SWord16 -> SBool)   -- takes too long!
+check = do print =<< prove (qrem :: SWord8   -> SWord8   -> SBool)
+           print =<< prove (qrem :: SInt8    -> SInt8    -> SBool)
+           print =<< prove (qrem :: SInteger -> SInteger -> SBool)
diff --git a/SBVUnitTest/Examples/Puzzles/Temperature.hs b/SBVUnitTest/Examples/Puzzles/Temperature.hs
--- a/SBVUnitTest/Examples/Puzzles/Temperature.hs
+++ b/SBVUnitTest/Examples/Puzzles/Temperature.hs
@@ -15,25 +15,25 @@
 
 import Data.SBV
 
-type Temp = SWord16 -- larger than we need actually
+type Temp = SInteger
 
 -- convert celcius to fahrenheit, rounding up/down properly
 -- we have to be careful here to make sure rounding is done properly..
 d2f :: Temp -> Temp
 d2f d = 32 + ite (fr .>= 5) (1+fi) fi
-  where (fi, fr) = (18 * d) `bvQuotRem` 10
+  where (fi, fr) = (18 * d) `sQuotRem` 10
 
 -- puzzle: What 2 digit fahrenheit/celcius values are reverses of each other?
 revOf :: Temp -> SBool
 revOf c = swap (digits c) .== digits (d2f c)
-  where digits x = x `bvQuotRem` 10
+  where digits x = x `sQuotRem` 10
         swap (a, b) = (b, a)
 
-solve :: IO ()
-solve = do res <- allSat $ revOf `fmap` exists_
-           cnt <- displayModels disp res
-           putStrLn $ "Found " ++ show cnt ++ " solutions."
-     where disp :: Int -> (Bool, Word16) -> IO ()
+puzzle :: IO ()
+puzzle = do res <- allSat $ revOf `fmap` exists_
+            cnt <- displayModels disp res
+            putStrLn $ "Found " ++ show cnt ++ " solutions."
+     where disp :: Int -> (Bool, Integer) -> IO ()
            disp _ (_, x) = putStrLn $ " " ++ show x ++ "C --> " ++ show (round f :: Integer) ++ "F (exact value: " ++ show f ++ "F)"
               where f :: Double
                     f  = 32 + (9 * fromIntegral x) / 5
diff --git a/SBVUnitTest/GoldFiles/temperature.gold b/SBVUnitTest/GoldFiles/temperature.gold
--- a/SBVUnitTest/GoldFiles/temperature.gold
+++ b/SBVUnitTest/GoldFiles/temperature.gold
@@ -1,2 +1,5 @@
-Satisfiable. Model:
-  s0 = 28 :: SWord16
+Solution #1:
+  s0 = 16 :: SInteger
+Solution #2:
+  s0 = 28 :: SInteger
+Found 2 different solutions.
diff --git a/SBVUnitTest/SBVBasicTests.hs b/SBVUnitTest/SBVBasicTests.hs
new file mode 100644
--- /dev/null
+++ b/SBVUnitTest/SBVBasicTests.hs
@@ -0,0 +1,64 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Main
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- SBV library basic test suite; i.e., those tests that do not
+-- require the use of an external SMT solver.
+-----------------------------------------------------------------------------
+
+-- Nothing needs to be changed in this file, add test cases
+-- appropriately to SBVUnitTest.hs file, and they will be
+-- picked up here automagically
+module Main(main) where
+
+import Control.Monad    (unless, when)
+import System.Directory (doesDirectoryExist)
+import System.Exit      (exitWith, exitSuccess, ExitCode(..))
+import System.FilePath  ((</>))
+import System.IO        (stderr, hPutStrLn)
+import Test.HUnit       (Test(..), Counts(..), runTestText, PutText(..), showCounts)
+
+import Data.Version     (showVersion)
+import SBVTest          (SBVTestSuite(..), generateGoldCheck)
+import Paths_sbv        (getDataDir, version)
+
+import SBVTestCollection    (allTestCases)
+import SBVUnitTestBuildTime (buildTime)
+
+testCollection :: [(String, SBVTestSuite)]
+testCollection = [(n, s) | (n, False, s) <- allTestCases]
+
+main :: IO ()
+main = do putStrLn $ "*** SBVBasicTester, version: " ++ showVersion version ++ ", time stamp: " ++ buildTime
+          d <- getDataDir 
+          run $ d </> "SBVUnitTest" </> "GoldFiles"
+
+checkGoldDir :: FilePath -> IO ()
+checkGoldDir gd = do e <- doesDirectoryExist gd
+                     unless e $ do putStrLn "*** Cannot locate gold file repository!"
+                                   putStrLn "*** Please call with one argument, the directory name of the gold files."
+                                   putStrLn "*** Cannot run test cases, exiting."
+                                   exitWith $ ExitFailure 1
+
+run :: FilePath -> IO ()
+run gd = do putStrLn $ "*** Starting SBV basic tests..\n*** Gold files at: " ++ show gd
+            checkGoldDir gd
+            (cts, _) <- runTestText (PutText put ()) $ TestList $ map (mkTst . snd) testCollection
+            hPutStrLn stderr $ showCounts cts
+            decide cts
+  where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd False
+        put s _ st = length s `seq` return st
+
+decide :: Counts -> IO ()
+decide (Counts c t e f) = do
+        when (c /= t) $ putStrLn $ "*** Not all test cases were tried. (Only tested " ++ show t ++ " of " ++ show c ++ ")"
+        when (e /= 0) $ putStrLn $ "*** " ++ show e ++ " (of " ++ show c ++ ") test cases in error."
+        when (f /= 0) $ putStrLn $ "*** " ++ show f ++ " (of " ++ show c ++ ") test cases failed."
+        if c == t && e == 0 && f == 0
+           then do putStrLn $ "All " ++ show c ++ " test cases successfully passed."
+                   exitSuccess
+           else exitWith $ ExitFailure 2
diff --git a/SBVUnitTest/SBVTestCollection.hs b/SBVUnitTest/SBVTestCollection.hs
new file mode 100644
--- /dev/null
+++ b/SBVUnitTest/SBVTestCollection.hs
@@ -0,0 +1,106 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Main
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- SBV test collection
+-----------------------------------------------------------------------------
+
+module SBVTestCollection(allTestCases) where
+
+import SBVTest
+
+-- To add a new collection of tests, import below and add to allTestCases variable
+import qualified TestSuite.Arrays.Memory                  as T01_01(testSuite)
+import qualified TestSuite.Basics.ArithNoSolver           as T02_01(testSuite)
+import qualified TestSuite.Basics.ArithSolver             as T02_02(testSuite)
+import qualified TestSuite.Basics.BasicTests              as T02_03(testSuite)
+import qualified TestSuite.Basics.Higher                  as T02_04(testSuite)
+import qualified TestSuite.Basics.Index                   as T02_05(testSuite)
+import qualified TestSuite.Basics.ProofTests              as T02_06(testSuite)
+import qualified TestSuite.Basics.QRem                    as T02_07(testSuite)
+import qualified TestSuite.BitPrecise.BitTricks           as T03_01(testSuite)
+import qualified TestSuite.BitPrecise.Legato              as T03_02(testSuite)
+import qualified TestSuite.BitPrecise.MergeSort           as T03_03(testSuite)
+import qualified TestSuite.BitPrecise.PrefixSum           as T03_04(testSuite)
+import qualified TestSuite.CRC.CCITT                      as T04_01(testSuite)
+import qualified TestSuite.CRC.CCITT_Unidir               as T04_02(testSuite)
+import qualified TestSuite.CRC.GenPoly                    as T04_03(testSuite)
+import qualified TestSuite.CRC.Parity                     as T04_04(testSuite)
+import qualified TestSuite.CRC.USB5                       as T04_05(testSuite)
+import qualified TestSuite.CodeGeneration.AddSub          as T05_01(testSuite)
+import qualified TestSuite.CodeGeneration.CgTests         as T05_02(testSuite)
+import qualified TestSuite.CodeGeneration.CRC_USB5        as T05_03(testSuite)
+import qualified TestSuite.CodeGeneration.Fibonacci       as T05_04(testSuite)
+import qualified TestSuite.CodeGeneration.GCD             as T05_05(testSuite)
+import qualified TestSuite.CodeGeneration.PopulationCount as T05_06(testSuite)
+import qualified TestSuite.CodeGeneration.Uninterpreted   as T05_07(testSuite)
+import qualified TestSuite.Crypto.AES                     as T06_01(testSuite)
+import qualified TestSuite.Crypto.RC4                     as T06_02(testSuite)
+import qualified TestSuite.Existentials.CRCPolynomial     as T07_01(testSuite)
+import qualified TestSuite.Polynomials.Polynomials        as T08_01(testSuite)
+import qualified TestSuite.Puzzles.Coins                  as T09_01(testSuite)
+import qualified TestSuite.Puzzles.Counts                 as T09_02(testSuite)
+import qualified TestSuite.Puzzles.DogCatMouse            as T09_03(testSuite)
+import qualified TestSuite.Puzzles.Euler185               as T09_04(testSuite)
+import qualified TestSuite.Puzzles.MagicSquare            as T09_05(testSuite)
+import qualified TestSuite.Puzzles.NQueens                as T09_06(testSuite)
+import qualified TestSuite.Puzzles.PowerSet               as T09_07(testSuite)
+import qualified TestSuite.Puzzles.Sudoku                 as T09_08(testSuite)
+import qualified TestSuite.Puzzles.Temperature            as T09_09(testSuite)
+import qualified TestSuite.Puzzles.U2Bridge               as T09_10(testSuite)
+import qualified TestSuite.Uninterpreted.AUF              as T10_01(testSuite)
+import qualified TestSuite.Uninterpreted.Function         as T10_02(testSuite)
+import qualified TestSuite.Uninterpreted.Uninterpreted    as T10_03(testSuite)
+
+-- Bool says whether we need a real SMT solver to run this test
+-- Note that it's ok to say True even if an SMT solver is *not*
+-- needed, but we'd like most things to be targeted False so that
+-- those tests can be run as part of cabal.
+allTestCases :: [(String, Bool, SBVTestSuite)]
+allTestCases = [
+       ("mem",         True,  T01_01.testSuite)
+     , ("arithCF",     False, T02_01.testSuite)
+     , ("arith",       True,  T02_02.testSuite)
+     , ("basic",       False, T02_03.testSuite)
+     , ("higher",      True,  T02_04.testSuite)
+     , ("index",       True,  T02_05.testSuite)
+     , ("proof",       True,  T02_06.testSuite)
+     , ("qrem",        True,  T02_07.testSuite)
+     , ("bitTricks",   True,  T03_01.testSuite)
+     , ("legato",      False, T03_02.testSuite)
+     , ("mergeSort",   False, T03_03.testSuite)
+     , ("prefixSum",   True,  T03_04.testSuite)
+     , ("ccitt",       False, T04_01.testSuite)
+     , ("ccitt2",      True,  T04_02.testSuite)
+     , ("genPoly",     True,  T04_03.testSuite)
+     , ("parity",      True,  T04_04.testSuite)
+     , ("usb5",        True,  T04_05.testSuite)
+     , ("addSub",      False, T05_01.testSuite)
+     , ("cgtest",      False, T05_02.testSuite)
+     , ("cgUSB5",      False, T05_03.testSuite)
+     , ("fib",         False, T05_04.testSuite)
+     , ("gcd",         False, T05_05.testSuite)
+     , ("popCount",    False, T05_06.testSuite)
+     , ("cgUninterp",  False, T05_07.testSuite)
+     , ("aes",         False, T06_01.testSuite)
+     , ("rc4",         True,  T06_02.testSuite)
+     , ("existPoly",   False, T07_01.testSuite)
+     , ("poly",        True,  T08_01.testSuite)
+     , ("coins",       False, T09_01.testSuite)
+     , ("counts",      False, T09_02.testSuite)
+     , ("dogCatMouse", True,  T09_03.testSuite)
+     , ("euler185",    True,  T09_04.testSuite)
+     , ("magicSquare", True,  T09_05.testSuite)
+     , ("nQueens",     True,  T09_06.testSuite)
+     , ("powerset",    True,  T09_07.testSuite)
+     , ("sudoku",      True,  T09_08.testSuite)
+     , ("temperature", True,  T09_09.testSuite)
+     , ("u2bridge",    True,  T09_10.testSuite)
+     , ("auf1",        True,  T10_01.testSuite)
+     , ("auf2",        True,  T10_02.testSuite)
+     , ("unint",       True,  T10_03.testSuite)
+     ]
diff --git a/SBVUnitTest/SBVUnitTest.hs b/SBVUnitTest/SBVUnitTest.hs
--- a/SBVUnitTest/SBVUnitTest.hs
+++ b/SBVUnitTest/SBVUnitTest.hs
@@ -23,108 +23,19 @@
 import Paths_sbv            (getDataDir, version)
 
 import SBVUnitTestBuildTime (buildTime)
-
--- To add a new collection of tests, import below and add to testCollection variable
-import qualified TestSuite.Arrays.Memory                  as T01_01(testSuite)
-import qualified TestSuite.Basics.Arithmetic              as T02_01(testSuite)
-import qualified TestSuite.Basics.BasicTests              as T02_02(testSuite)
-import qualified TestSuite.Basics.Higher                  as T02_03(testSuite)
-import qualified TestSuite.Basics.Index                   as T02_04(testSuite)
-import qualified TestSuite.Basics.ProofTests              as T02_05(testSuite)
-import qualified TestSuite.Basics.QRem                    as T02_06(testSuite)
-import qualified TestSuite.BitPrecise.BitTricks           as T03_01(testSuite)
-import qualified TestSuite.BitPrecise.Legato              as T03_02(testSuite)
-import qualified TestSuite.BitPrecise.MergeSort           as T03_03(testSuite)
-import qualified TestSuite.BitPrecise.PrefixSum           as T03_04(testSuite)
-import qualified TestSuite.CRC.CCITT                      as T04_01(testSuite)
-import qualified TestSuite.CRC.CCITT_Unidir               as T04_02(testSuite)
-import qualified TestSuite.CRC.GenPoly                    as T04_03(testSuite)
-import qualified TestSuite.CRC.Parity                     as T04_04(testSuite)
-import qualified TestSuite.CRC.USB5                       as T04_05(testSuite)
-import qualified TestSuite.CodeGeneration.AddSub          as T05_01(testSuite)
-import qualified TestSuite.CodeGeneration.CgTests         as T05_02(testSuite)
-import qualified TestSuite.CodeGeneration.CRC_USB5        as T05_03(testSuite)
-import qualified TestSuite.CodeGeneration.Fibonacci       as T05_04(testSuite)
-import qualified TestSuite.CodeGeneration.GCD             as T05_05(testSuite)
-import qualified TestSuite.CodeGeneration.PopulationCount as T05_06(testSuite)
-import qualified TestSuite.CodeGeneration.Uninterpreted   as T05_07(testSuite)
-import qualified TestSuite.Crypto.AES                     as T06_01(testSuite)
-import qualified TestSuite.Crypto.RC4                     as T06_02(testSuite)
-import qualified TestSuite.Existentials.CRCPolynomial     as T07_01(testSuite)
-import qualified TestSuite.Polynomials.Polynomials        as T08_01(testSuite)
-import qualified TestSuite.Puzzles.Coins                  as T09_01(testSuite)
-import qualified TestSuite.Puzzles.Counts                 as T09_02(testSuite)
-import qualified TestSuite.Puzzles.DogCatMouse            as T09_03(testSuite)
-import qualified TestSuite.Puzzles.Euler185               as T09_04(testSuite)
-import qualified TestSuite.Puzzles.MagicSquare            as T09_05(testSuite)
-import qualified TestSuite.Puzzles.NQueens                as T09_06(testSuite)
-import qualified TestSuite.Puzzles.PowerSet               as T09_07(testSuite)
-import qualified TestSuite.Puzzles.Sudoku                 as T09_08(testSuite)
-import qualified TestSuite.Puzzles.Temperature            as T09_09(testSuite)
-import qualified TestSuite.Puzzles.U2Bridge               as T09_10(testSuite)
-import qualified TestSuite.Uninterpreted.AUF              as T10_01(testSuite)
-import qualified TestSuite.Uninterpreted.Function         as T10_02(testSuite)
-import qualified TestSuite.Uninterpreted.Uninterpreted    as T10_03(testSuite)
-
-testCollection :: [(String, SBVTestSuite)]
-testCollection = [
-       ("mem",         T01_01.testSuite)
-     , ("arith",       T02_01.testSuite)
-     , ("basic",       T02_02.testSuite)
-     , ("higher",      T02_03.testSuite)
-     , ("index",       T02_04.testSuite)
-     , ("proof",       T02_05.testSuite)
-     , ("qrem",        T02_06.testSuite)
-     , ("bitTricks",   T03_01.testSuite)
-     , ("legato",      T03_02.testSuite)
-     , ("mergeSort",   T03_03.testSuite)
-     , ("prefixSum",   T03_04.testSuite)
-     , ("ccitt",       T04_01.testSuite)
-     , ("ccitt2",      T04_02.testSuite)
-     , ("genPoly",     T04_03.testSuite)
-     , ("parity",      T04_04.testSuite)
-     , ("usb5",        T04_05.testSuite)
-     , ("addSub",      T05_01.testSuite)
-     , ("cgtest",      T05_02.testSuite)
-     , ("cgUSB5",      T05_03.testSuite)
-     , ("fib",         T05_04.testSuite)
-     , ("gcd",         T05_05.testSuite)
-     , ("popCount",    T05_06.testSuite)
-     , ("cgUninterp",  T05_07.testSuite)
-     , ("aes",         T06_01.testSuite)
-     , ("rc4",         T06_02.testSuite)
-     , ("existPoly",   T07_01.testSuite)
-     , ("poly",        T08_01.testSuite)
-     , ("coins",       T09_01.testSuite)
-     , ("counts",      T09_02.testSuite)
-     , ("dogCatMouse", T09_03.testSuite)
-     , ("euler185",    T09_04.testSuite)
-     , ("magicSquare", T09_05.testSuite)
-     , ("nQueens",     T09_06.testSuite)
-     , ("powerset",    T09_07.testSuite)
-     , ("sudoku",      T09_08.testSuite)
-     , ("temperature", T09_09.testSuite)
-     , ("u2bridge",    T09_10.testSuite)
-     , ("auf1",        T10_01.testSuite)
-     , ("auf2",        T10_02.testSuite)
-     , ("unint",       T10_03.testSuite)
-     ]
-
--- No user serviceable parts below..
+import SBVTestCollection    (allTestCases)
 
 main :: IO ()
 main = do putStrLn $ "*** SBVUnitTester, version: " ++ showVersion version ++ ", time stamp: " ++ buildTime
           tgts <- getArgs
           case tgts of
             [x] | x `elem` ["-h", "--help", "-?"]
-                   -> putStrLn "Usage: SBVUnitTests [-l] [targets]" -- Not quite right, but sufficient
+                   -> putStrLn "Usage: SBVUnitTests [-l(ist)] [-s(kipCF)] [targets]" -- Not quite right, but sufficient
             ["-l"] -> showTargets
             -- undocumented really
-            ("-c":ts) -> createGolds (unwords ts)
-            _      -> run tgts False []
-
-createGolds :: String -> IO ()
-createGolds tgts = run (words tgts) True ["SBVUnitTest/GoldFiles"]
+            ("-c":ts) -> run ts   False True ["SBVUnitTest/GoldFiles"]
+            ("-s":ts) -> run ts   True False []
+            _         -> run tgts False False []
 
 checkGoldDir :: FilePath -> IO ()
 checkGoldDir gd = do e <- doesDirectoryExist gd
@@ -134,26 +45,31 @@
                                    exitWith $ ExitFailure 1
 
 allTargets :: [String]
-allTargets = map fst testCollection
+allTargets = [s | (s, _, _) <- allTestCases]
 
 showTargets :: IO ()
 showTargets = do putStrLn "Known test targets are:"
                  mapM_ (putStrLn . ("\t" ++))  allTargets
 
-run :: [String] -> Bool -> [String] -> IO ()
-run targets shouldCreate [gd] =
+run :: [String] -> Bool -> Bool -> [String] -> IO ()
+run targets skipCF shouldCreate [gd] =
         do mapM_ checkTgt targets
            putStrLn $ "*** Starting SBV unit tests..\n*** Gold files at: " ++ show gd
            checkGoldDir gd
-           cts <- runTestTT $ TestList $ map mkTst [c | (tc, c) <- testCollection, select tc]
+           cts <- runTestTT $ TestList $ map mkTst [c | (tc, needsSolver, c) <- allTestCases, select needsSolver tc]
            decide shouldCreate cts
   where mkTst (SBVTestSuite f) = f $ generateGoldCheck gd shouldCreate
-        select tc = null targets || tc `elem` targets
+        select needsSolver tc
+           | not included = False
+           | shouldCreate = True
+           | needsSolver  = True
+           | True         = not skipCF
+          where included = null targets || tc `elem` targets
         checkTgt t | t `elem` allTargets = return ()
                    | True                = do putStrLn $ "*** Unknown test target: " ++ show t
                                               exitWith $ ExitFailure 1
-run targets shouldCreate [] = getDataDir >>= \d -> run targets shouldCreate [d </> "SBVUnitTest" </> "GoldFiles"]
-run _       _            _  = error "SBVUnitTests.run: impossible happened!"
+run targets skipCF shouldCreate [] = getDataDir >>= \d -> run targets skipCF shouldCreate [d </> "SBVUnitTest" </> "GoldFiles"]
+run _       _      _            _  = error "SBVUnitTests.run: impossible happened!"
 
 decide :: Bool -> Counts -> IO ()
 decide shouldCreate (Counts c t e f) = do
diff --git a/SBVUnitTest/SBVUnitTestBuildTime.hs b/SBVUnitTest/SBVUnitTestBuildTime.hs
--- a/SBVUnitTest/SBVUnitTestBuildTime.hs
+++ b/SBVUnitTest/SBVUnitTestBuildTime.hs
@@ -2,4 +2,4 @@
 module SBVUnitTestBuildTime (buildTime) where
 
 buildTime :: String
-buildTime = "Thu Jul 19 22:00:35 PDT 2012"
+buildTime = "Thu Oct 18 20:24:21 PDT 2012"
diff --git a/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs
new file mode 100644
--- /dev/null
+++ b/SBVUnitTest/TestSuite/Basics/ArithNoSolver.hs
@@ -0,0 +1,287 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  TestSuite.Basics.ArithNoSolver
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Test suite for basic concrete arithmetic, i.e., testing all
+-- the constant folding based arithmetic implementation in SBV
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE Rank2Types    #-}
+{-# LANGUAGE TupleSections #-}
+
+module TestSuite.Basics.ArithNoSolver(testSuite) where
+
+import Data.SBV
+
+import SBVTest
+
+-- Test suite
+testSuite :: SBVTestSuite
+testSuite = mkTestSuite $ \_ -> test $
+        genReals
+     ++ genQRems
+     ++ genBinTest  "+"                (+)
+     ++ genBinTest  "-"                (-)
+     ++ genBinTest  "*"                (*)
+     ++ genUnTest   "negate"           negate
+     ++ genUnTest   "abs"              abs
+     ++ genUnTest   "signum"           signum
+     ++ genBinTest  ".&."              (.&.)
+     ++ genBinTest  ".|."              (.|.)
+     ++ genBoolTest "<"                (<)  (.<)
+     ++ genBoolTest "<="               (<=) (.<=)
+     ++ genBoolTest ">"                (>)  (.>)
+     ++ genBoolTest ">="               (>=) (.>=)
+     ++ genBoolTest "=="               (==) (.==)
+     ++ genBoolTest "/="               (/=) (./=)
+     ++ genBinTest  "xor"              xor
+     ++ genUnTest   "complement"       complement
+     ++ genIntTest  "shift"            shift
+     ++ genIntTest  "rotate"           rotate
+     ++ genIntTestS "setBit"           setBit
+     ++ genIntTestS "clearBit"         clearBit
+     ++ genIntTestS "complementBit"    complementBit
+     ++ genIntTest  "shift"            shift
+     ++ genIntTestS "shiftL"           shiftL
+     ++ genIntTestS "shiftR"           shiftR
+     ++ genIntTest  "rotate"           rotate
+     ++ genIntTestS "rotateL"          rotateL
+     ++ genIntTestS "rotateR"          rotateR
+     ++ genBlasts
+     ++ genCasts
+
+genBinTest :: String -> (forall a. Bits a => a -> a -> a) -> [Test]
+genBinTest nm op = map mkTest $
+        zipWith pair [(show x, show y, x `op` y) | x <- w8s,  y <- w8s ] [x `op` y | x <- sw8s,  y <- sw8s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s,  y <- i8s ] [x `op` y | x <- si8s,  y <- si8s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]
+  where pair (x, y, a) b   = (x, y, show (fromIntegral a `asTypeOf` b) == show b)
+        mkTest (x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
+
+genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]
+genBoolTest nm op opS = map mkTest $
+        zipWith pair [(show x, show y, x `op` y) | x <- w8s,  y <- w8s ] [x `opS` y | x <- sw8s,  y <- sw8s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s,  y <- i8s ] [x `opS` y | x <- si8s,  y <- si8s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s]
+     ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs]
+  where pair (x, y, a) b   = (x, y, Just a == unliteral b)
+        mkTest (x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
+
+genUnTest :: String -> (forall a. Bits a => a -> a) -> [Test]
+genUnTest nm op = map mkTest $
+        zipWith pair [(show x, op x) | x <- w8s ] [op x | x <- sw8s ]
+     ++ zipWith pair [(show x, op x) | x <- w16s] [op x | x <- sw16s]
+     ++ zipWith pair [(show x, op x) | x <- w32s] [op x | x <- sw32s]
+     ++ zipWith pair [(show x, op x) | x <- w64s] [op x | x <- sw64s]
+     ++ zipWith pair [(show x, op x) | x <- i8s ] [op x | x <- si8s ]
+     ++ zipWith pair [(show x, op x) | x <- i16s] [op x | x <- si16s]
+     ++ zipWith pair [(show x, op x) | x <- i32s] [op x | x <- si32s]
+     ++ zipWith pair [(show x, op x) | x <- i64s] [op x | x <- si64s]
+     ++ zipWith pair [(show x, op x) | x <- iUBs] [op x | x <- siUBs]
+  where pair (x, a) b   = (x, show (fromIntegral a `asTypeOf` b) == show b)
+        mkTest (x, s) = "arithCF-" ++ nm ++ "." ++ x ~: s `showsAs` "True"
+
+genIntTest :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]
+genIntTest nm op = map mkTest $
+        zipWith pair [("u8",  show x, show y, x `op` y) | x <- w8s,  y <- is] [x `op` y | x <- sw8s,  y <- is]
+     ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- is] [x `op` y | x <- sw16s, y <- is]
+     ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is] [x `op` y | x <- sw32s, y <- is]
+     ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is] [x `op` y | x <- sw64s, y <- is]
+     ++ zipWith pair [("s8",  show x, show y, x `op` y) | x <- i8s,  y <- is] [x `op` y | x <- si8s,  y <- is]
+     ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is] [x `op` y | x <- si16s, y <- is]
+     ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is] [x `op` y | x <- si32s, y <- is]
+     ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is] [x `op` y | x <- si64s, y <- is]
+     ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- is] [x `op` y | x <- siUBs, y <- is]
+  where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)
+        mkTest (t, x, y, a, b, s) = "arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
+        is = [-10 .. 10]
+
+genIntTestS :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]
+genIntTestS nm op = map mkTest $
+        zipWith pair [("u8",  show x, show y, x `op` y) | x <- w8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s,  y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s8",  show x, show y, x `op` y) | x <- i8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s,  y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]
+     ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]]              [x `op` y | x <- siUBs, y <- [0 .. 10             ]]
+  where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)
+        mkTest (t, x, y, a, b, s) = "arithCF-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
+
+genBlasts :: [Test]
+genBlasts = map mkTest $
+             [(show x, fromBitsLE (blastLE x) .== x) | x <- sw8s ]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw8s ]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si8s ]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si8s ]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s]
+          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s]
+          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s]
+  where mkTest (x, r) = "blast-" ++ show x ~: r `showsAs` "True"
+
+genCasts :: [Test]
+genCasts = map mkTest $
+            [(show x, unsignCast (signCast x) .== x) | x <- sw8s ]
+         ++ [(show x, unsignCast (signCast x) .== x) | x <- sw16s]
+         ++ [(show x, unsignCast (signCast x) .== x) | x <- sw32s]
+         ++ [(show x, unsignCast (signCast x) .== x) | x <- sw64s]
+         ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]
+         ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]
+         ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]
+         ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]
+         ++ [(show x, signCast (unsignCast x) .== x) | x <- si32s]
+         ++ [(show x, signCast (unsignCast x) .== x) | x <- si64s]
+         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw8s ]
+         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw16s]
+         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw32s]
+         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw64s]
+         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si8s ]
+         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si16s]
+         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si32s]
+         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si64s]
+  where mkTest (x, r) = "cast-" ++ show x ~: r `showsAs` "True"
+
+genQRems :: [Test]
+genQRems = map mkTest $
+        zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- w8s,  y <- w8s ]                 [x `sDivMod`  y | x <- sw8s,  y <- sw8s ]
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- w16s, y <- w16s]                 [x `sDivMod`  y | x <- sw16s, y <- sw16s]
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- w32s, y <- w32s]                 [x `sDivMod`  y | x <- sw32s, y <- sw32s]
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- w64s, y <- w64s]                 [x `sDivMod`  y | x <- sw64s, y <- sw64s]
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- i8s,  y <- i8s , noOverflow x y] [x `sDivMod`  y | x <- si8s,  y <- si8s , noOverflow x y]
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- i16s, y <- i16s, noOverflow x y] [x `sDivMod`  y | x <- si16s, y <- si16s, noOverflow x y]
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- i32s, y <- i32s, noOverflow x y] [x `sDivMod`  y | x <- si32s, y <- si32s, noOverflow x y]
+     ++ (if divModInt64Bug    -- see below
+            then []
+            else zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- i64s, y <- i64s, noOverflow x y] [x `sDivMod`  y | x <- si64s, y <- si64s, noOverflow x y]
+        )
+     ++ zipWith pair [("divMod",  show x, show y, x `divMod'`  y) | x <- iUBs, y <- iUBs]                 [x `sDivMod`  y | x <- siUBs, y <- siUBs]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w8s,  y <- w8s ]                 [x `sQuotRem` y | x <- sw8s,  y <- sw8s ]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w16s, y <- w16s]                 [x `sQuotRem` y | x <- sw16s, y <- sw16s]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w32s, y <- w32s]                 [x `sQuotRem` y | x <- sw32s, y <- sw32s]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- w64s, y <- w64s]                 [x `sQuotRem` y | x <- sw64s, y <- sw64s]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i8s,  y <- i8s , noOverflow x y] [x `sQuotRem` y | x <- si8s,  y <- si8s , noOverflow x y]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i16s, y <- i16s, noOverflow x y] [x `sQuotRem` y | x <- si16s, y <- si16s, noOverflow x y]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i32s, y <- i32s, noOverflow x y] [x `sQuotRem` y | x <- si32s, y <- si32s, noOverflow x y]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- i64s, y <- i64s, noOverflow x y] [x `sQuotRem` y | x <- si64s, y <- si64s, noOverflow x y]
+     ++ zipWith pair [("quotRem", show x, show y, x `quotRem'` y) | x <- iUBs, y <- iUBs]                 [x `sQuotRem` y | x <- siUBs, y <- siUBs]
+  where divMod'  x y = if y == 0 then (0, x) else x `divMod`  y
+        quotRem' x y = if y == 0 then (0, x) else x `quotRem` y
+        pair (nm, x, y, (r1, r2)) (e1, e2)   = (nm, x, y, show (fromIntegral r1 `asTypeOf` e1, fromIntegral r2 `asTypeOf` e2) == show (e1, e2))
+        mkTest (nm, x, y, s) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
+        -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for bounded signed types; so avoid that case
+        noOverflow x y = not (x == minBound && y == -1)
+
+genReals :: [Test]
+genReals = map mkTest $
+        map ("+",)  (zipWith pair [(show x, show y, x +  y) | x <- rs, y <- rs        ] [x +   y | x <- srs,  y <- srs                       ])
+     ++ map ("-",)  (zipWith pair [(show x, show y, x -  y) | x <- rs, y <- rs        ] [x -   y | x <- srs,  y <- srs                       ])
+     ++ map ("*",)  (zipWith pair [(show x, show y, x *  y) | x <- rs, y <- rs        ] [x *   y | x <- srs,  y <- srs                       ])
+     ++ map ("<",)  (zipWith pair [(show x, show y, x <  y) | x <- rs, y <- rs        ] [x .<  y | x <- srs,  y <- srs                       ])
+     ++ map ("<=",) (zipWith pair [(show x, show y, x <= y) | x <- rs, y <- rs        ] [x .<= y | x <- srs,  y <- srs                       ])
+     ++ map (">",)  (zipWith pair [(show x, show y, x >  y) | x <- rs, y <- rs        ] [x .>  y | x <- srs,  y <- srs                       ])
+     ++ map (">=",) (zipWith pair [(show x, show y, x >= y) | x <- rs, y <- rs        ] [x .>= y | x <- srs,  y <- srs                       ])
+     ++ map ("==",) (zipWith pair [(show x, show y, x == y) | x <- rs, y <- rs        ] [x .== y | x <- srs,  y <- srs                       ])
+     ++ map ("/=",) (zipWith pair [(show x, show y, x /= y) | x <- rs, y <- rs        ] [x ./= y | x <- srs,  y <- srs                       ])
+     ++ map ("/",)  (zipWith pair [(show x, show y, x /  y) | x <- rs, y <- rs, y /= 0] [x / y   | x <- srs,  y <- srs, unliteral y /= Just 0])
+  where pair (x, y, a) b   = (x, y, Just a == unliteral b)
+        mkTest (nm, (x, y, s)) = "arithCF-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
+
+-- Concrete test data
+xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]
+xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound)
+xsSigned   = xsUnsigned ++ [-5 .. 5]
+
+w8s :: [Word8]
+w8s = xsUnsigned
+
+sw8s :: [SWord8]
+sw8s = xsUnsigned
+
+w16s :: [Word16]
+w16s = xsUnsigned
+
+sw16s :: [SWord16]
+sw16s = xsUnsigned
+
+w32s :: [Word32]
+w32s = xsUnsigned
+
+sw32s :: [SWord32]
+sw32s = xsUnsigned
+
+w64s :: [Word64]
+w64s = xsUnsigned
+
+sw64s :: [SWord64]
+sw64s = xsUnsigned
+
+i8s :: [Int8]
+i8s = xsSigned
+
+si8s :: [SInt8]
+si8s = xsSigned
+
+i16s :: [Int16]
+i16s = xsSigned
+
+si16s :: [SInt16]
+si16s = xsSigned
+
+i32s :: [Int32]
+i32s = xsSigned
+
+si32s :: [SInt32]
+si32s = xsSigned
+
+i64s :: [Int64]
+i64s = xsSigned
+
+si64s :: [SInt64]
+si64s = xsSigned
+
+iUBs :: [Integer]
+iUBs = [-1000000 .. -999995] ++ [-5 .. 5] ++ [999995 ..  1000000]
+
+siUBs :: [SInteger]
+siUBs = map literal iUBs
+
+rs :: [AlgReal]
+rs = [fromRational (i % d) | i <- is, d <- ds]
+ where is = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 ..  1000001]
+       ds = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000]
+
+srs :: [SReal]
+srs = map literal rs
+
+
+-- On 32 bit installations of GHC, divMod is buggy for Int64
+-- Thus causing our tests to fail. See ticket: http://hackage.haskell.org/trac/ghc/ticket/7233
+-- Luckily, it's easy to detect it and sidestep it until GHC is appropriately patched
+divModInt64Bug :: Bool
+divModInt64Bug = (1 `div` (minBound::Int64)) /= -1   -- Bug causes this expression to evaluate to 1
diff --git a/SBVUnitTest/TestSuite/Basics/ArithSolver.hs b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs
new file mode 100644
--- /dev/null
+++ b/SBVUnitTest/TestSuite/Basics/ArithSolver.hs
@@ -0,0 +1,270 @@
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  TestSuite.Basics.ArithSolver
+-- Copyright   :  (c) Levent Erkok
+-- License     :  BSD3
+-- Maintainer  :  erkokl@gmail.com
+-- Stability   :  experimental
+--
+-- Test suite for basic non-concrete arithmetic, i.e., testing all
+-- basic arithmetic reasoning using an SMT solver without any
+-- constant folding.
+-----------------------------------------------------------------------------
+
+{-# LANGUAGE Rank2Types    #-}
+{-# LANGUAGE TupleSections #-}
+
+module TestSuite.Basics.ArithSolver(testSuite) where
+
+import Data.SBV
+
+import SBVTest
+
+-- Test suite
+testSuite :: SBVTestSuite
+testSuite = mkTestSuite $ \_ -> test $
+        genReals
+     ++ genQRems
+     ++ genBinTest  True   "+"                (+)
+     ++ genBinTest  True   "-"                (-)
+     ++ genBinTest  True   "*"                (*)
+     ++ genUnTest   True   "negate"           negate
+     ++ genUnTest   True   "abs"              abs
+     ++ genUnTest   True   "signum"           signum
+     ++ genBinTest  False  ".&."              (.&.)
+     ++ genBinTest  False  ".|."              (.|.)
+     ++ genBoolTest        "<"                (<)  (.<)
+     ++ genBoolTest        "<="               (<=) (.<=)
+     ++ genBoolTest        ">"                (>)  (.>)
+     ++ genBoolTest        ">="               (>=) (.>=)
+     ++ genBoolTest        "=="               (==) (.==)
+     ++ genBoolTest        "/="               (/=) (./=)
+     ++ genBinTest  False  "xor"              xor
+     ++ genUnTest   False  "complement"       complement
+     ++ genIntTest         "shift"            shift
+     ++ genIntTest         "rotate"           rotate
+     ++ genIntTestS False  "setBit"           setBit
+     ++ genIntTestS False  "clearBit"         clearBit
+     ++ genIntTestS False  "complementBit"    complementBit
+     ++ genIntTest         "shift"            shift
+     ++ genIntTestS True   "shiftL"           shiftL
+     ++ genIntTestS True   "shiftR"           shiftR
+     ++ genIntTest         "rotate"           rotate
+     ++ genIntTestS True   "rotateL"          rotateL
+     ++ genIntTestS True   "rotateR"          rotateR
+     ++ genBlasts
+     ++ genCasts
+
+
+genBinTest :: Bool -> String -> (forall a. Bits a => a -> a -> a) -> [Test]
+genBinTest unboundedOK nm op = map mkTest $  [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s,  y <- w8s ]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s,  y <- i8s ]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]
+                                          ++ [(show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- iUBs]
+  where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t
+        mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]
+                                      constrain $ a .== literal x
+                                      constrain $ b .== literal y
+                                      return $ literal r .== a `op` b
+
+genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]
+genBoolTest nm op opS = map mkTest $  [(show x, show y, mkThm2 x y (x `op` y)) | x <- w8s,  y <- w8s ]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- w16s]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- w32s]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- w64s]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i8s,  y <- i8s ]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- i16s]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- i32s]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- i64s]
+                                   ++ [(show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- iUBs]
+  where mkTest (x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t
+        mkThm2 x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]
+                                      constrain $ a .== literal x
+                                      constrain $ b .== literal y
+                                      return $ literal r .== a `opS` b
+
+genUnTest :: Bool -> String -> (forall a. Bits a => a -> a) -> [Test]
+genUnTest unboundedOK nm op = map mkTest $  [(show x, mkThm x (op x)) | x <- w8s ]
+                                         ++ [(show x, mkThm x (op x)) | x <- w16s]
+                                         ++ [(show x, mkThm x (op x)) | x <- w32s]
+                                         ++ [(show x, mkThm x (op x)) | x <- w64s]
+                                         ++ [(show x, mkThm x (op x)) | x <- i8s ]
+                                         ++ [(show x, mkThm x (op x)) | x <- i16s]
+                                         ++ [(show x, mkThm x (op x)) | x <- i32s]
+                                         ++ [(show x, mkThm x (op x)) | x <- i64s]
+                                         ++ [(show x, mkThm x (op x)) | unboundedOK, x <- iUBs]
+  where mkTest (x, t) = "arithmetic-" ++ nm ++ "." ++ x ~: assert t
+        mkThm x r = isTheorem $ do a <- free "x"
+                                   constrain $ a .== literal x
+                                   return $ literal r .== op a
+
+genIntTest :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]
+genIntTest nm op = map mkTest $  [("u8",  show x, show y, mkThm2 x y (x `op` y)) | x <- w8s,  y <- is]
+                              ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- is]
+                              ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- is]
+                              ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- is]
+                              ++ [("s8",  show x, show y, mkThm2 x y (x `op` y)) | x <- i8s,  y <- is]
+                              ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- is]
+                              ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- is]
+                              ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- is]
+                              ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | x <- iUBs, y <- is]
+  where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t
+        is = [-10 .. 10]
+        mkThm2 x y r = isTheorem $ do a <- free "x"
+                                      constrain $ a .== literal x
+                                      return $ literal r .== a `op` y
+
+
+genIntTestS :: Bool -> String -> (forall a. Bits a => a -> Int -> a) -> [Test]
+genIntTestS unboundedOK nm op = map mkTest $  [("u8",  show x, show y, mkThm2 x y (x `op` y)) | x <- w8s,  y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("u16", show x, show y, mkThm2 x y (x `op` y)) | x <- w16s, y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("u32", show x, show y, mkThm2 x y (x `op` y)) | x <- w32s, y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("u64", show x, show y, mkThm2 x y (x `op` y)) | x <- w64s, y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("s8",  show x, show y, mkThm2 x y (x `op` y)) | x <- i8s,  y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("s16", show x, show y, mkThm2 x y (x `op` y)) | x <- i16s, y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("s32", show x, show y, mkThm2 x y (x `op` y)) | x <- i32s, y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("s64", show x, show y, mkThm2 x y (x `op` y)) | x <- i64s, y <- [0 .. (bitSize x - 1)]]
+                                           ++ [("iUB", show x, show y, mkThm2 x y (x `op` y)) | unboundedOK, x <- iUBs, y <- [0 .. 10]]
+  where mkTest (l, x, y, t) = "arithmetic-" ++ nm ++ "." ++ l ++ "_" ++ x ++ "_" ++ y ~: assert t
+        mkThm2 x y r = isTheorem $ do a <- free "x"
+                                      constrain $ a .== literal x
+                                      return $ literal r .== a `op` y
+
+genBlasts :: [Test]
+genBlasts = map mkTest $  [(show x, mkThm fromBitsLE blastLE x) | x <- w8s ]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w8s ]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i8s ]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i8s ]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w16s]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w16s]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i16s]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i16s]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w32s]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w32s]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i32s]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i32s]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- w64s]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- w64s]
+                       ++ [(show x, mkThm fromBitsLE blastLE x) | x <- i64s]
+                       ++ [(show x, mkThm fromBitsBE blastBE x) | x <- i64s]
+  where mkTest (x, t) = "blast-" ++ show x ~: assert t
+        mkThm from to v = isTheorem $ do a <- free "x"
+                                         constrain $ a .== literal v
+                                         return $ a .== from (to a)
+
+genCasts :: [Test]
+genCasts = map mkTest $  [(show x, mkThm unsignCast signCast x) | x <- w8s ]
+                      ++ [(show x, mkThm unsignCast signCast x) | x <- w16s]
+                      ++ [(show x, mkThm unsignCast signCast x) | x <- w32s]
+                      ++ [(show x, mkThm unsignCast signCast x) | x <- w64s]
+                      ++ [(show x, mkThm signCast unsignCast x) | x <- i8s ]
+                      ++ [(show x, mkThm signCast unsignCast x) | x <- i16s]
+                      ++ [(show x, mkThm signCast unsignCast x) | x <- i8s ]
+                      ++ [(show x, mkThm signCast unsignCast x) | x <- i16s]
+                      ++ [(show x, mkThm signCast unsignCast x) | x <- i32s]
+                      ++ [(show x, mkThm signCast unsignCast x) | x <- i64s]
+                      ++ [(show x, mkFEq signCast   (fromBitsLE . blastLE) x) | x <- w8s ]
+                      ++ [(show x, mkFEq signCast   (fromBitsLE . blastLE) x) | x <- w16s]
+                      ++ [(show x, mkFEq signCast   (fromBitsLE . blastLE) x) | x <- w32s]
+                      ++ [(show x, mkFEq signCast   (fromBitsLE . blastLE) x) | x <- w64s]
+                      ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i8s ]
+                      ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i16s]
+                      ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i32s]
+                      ++ [(show x, mkFEq unsignCast (fromBitsLE . blastLE) x) | x <- i64s]
+  where mkTest (x, t) = "cast-" ++ show x ~: assert t
+        mkThm from to v = isTheorem $ do a <- free "x"
+                                         constrain $ a .== literal v
+                                         return $ a .== from (to a)
+        mkFEq f g v = isTheorem $ do a <- free "x"
+                                     constrain $ a .== literal v
+                                     return $ f a .== g a
+
+genReals :: [Test]
+genReals = map mkTest $  [("+",  show x, show y, mkThm2 (+)   x y (x +  y)) | x <- rs, y <- rs        ]
+                      ++ [("-",  show x, show y, mkThm2 (-)   x y (x -  y)) | x <- rs, y <- rs        ]
+                      ++ [("*",  show x, show y, mkThm2 (*)   x y (x *  y)) | x <- rs, y <- rs        ]
+                      ++ [("/",  show x, show y, mkThm2 (/)   x y (x /  y)) | x <- rs, y <- rs, y /= 0]
+                      ++ [("<",  show x, show y, mkThm2 (.<)  x y (x <  y)) | x <- rs, y <- rs        ]
+                      ++ [("<=", show x, show y, mkThm2 (.<=) x y (x <= y)) | x <- rs, y <- rs        ]
+                      ++ [(">",  show x, show y, mkThm2 (.>)  x y (x >  y)) | x <- rs, y <- rs        ]
+                      ++ [(">=", show x, show y, mkThm2 (.>=) x y (x >= y)) | x <- rs, y <- rs        ]
+                      ++ [("==", show x, show y, mkThm2 (.==) x y (x == y)) | x <- rs, y <- rs        ]
+                      ++ [("/=", show x, show y, mkThm2 (./=) x y (x /= y)) | x <- rs, y <- rs        ]
+  where mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t
+        mkThm2 op x y r = isTheorem $ do [a, b] <- mapM free ["x", "y"]
+                                         constrain $ a .== literal x
+                                         constrain $ b .== literal y
+                                         return $ literal r .== a `op` b
+
+genQRems :: [Test]
+genQRems = map mkTest $  [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- w8s,  y <- w8s ]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- w16s, y <- w16s]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- w32s, y <- w32s]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- w64s, y <- w64s]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- i8s,  y <- i8s , noOverflow x y]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- i16s, y <- i16s, noOverflow x y]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- i32s, y <- i32s, noOverflow x y]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- i64s, y <- i64s, noOverflow x y]
+                      ++ [("divMod",  show x, show y, mkThm2 sDivMod  x y (x `divMod'`  y)) | x <- iUBs, y <- iUBs]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w8s,  y <- w8s ]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w16s, y <- w16s]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w32s, y <- w32s]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- w64s, y <- w64s]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i8s,  y <- i8s , noOverflow x y]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i16s, y <- i16s, noOverflow x y]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i32s, y <- i32s, noOverflow x y]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- i64s, y <- i64s, noOverflow x y]
+                      ++ [("quotRem", show x, show y, mkThm2 sQuotRem x y (x `quotRem'` y)) | x <- iUBs, y <- iUBs]
+  where divMod'  x y = if y == 0 then (0, x) else x `divMod`  y
+        quotRem' x y = if y == 0 then (0, x) else x `quotRem` y
+        mkTest (nm, x, y, t) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: assert t
+        mkThm2 op x y (e1, e2) = isTheorem $ do [a, b] <- mapM free ["x", "y"]
+                                                constrain $ a .== literal x
+                                                constrain $ b .== literal y
+                                                return $ (literal e1, literal e2) .== a `op` b
+        -- Haskell's divMod and quotRem overflows if x == minBound and y == -1 for signed types; so avoid that case
+        noOverflow x y = not (x == minBound && y == -1)
+
+-- Concrete test data
+xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]
+xsUnsigned = [minBound, 0, maxBound]
+xsSigned   = xsUnsigned ++ [-1, 1]
+
+w8s :: [Word8]
+w8s = xsUnsigned
+
+w16s :: [Word16]
+w16s = xsUnsigned
+
+w32s :: [Word32]
+w32s = xsUnsigned
+
+w64s :: [Word64]
+w64s = xsUnsigned
+
+i8s :: [Int8]
+i8s = xsSigned
+
+i16s :: [Int16]
+i16s = xsSigned
+
+i32s :: [Int32]
+i32s = xsSigned
+
+i64s :: [Int64]
+i64s = xsSigned
+
+iUBs :: [Integer]
+iUBs = [-1000000] ++ [-1 .. 1] ++ [1000000]
+
+rs :: [AlgReal]
+rs = [fromRational (i % d) | i <- is, d <- ds]
+ where is = [-1000000] ++ [-1 .. 1] ++ [10000001]
+       ds = [5,100,1000000]
+
+{-# ANN module "HLint: ignore Reduce duplication" #-}
diff --git a/SBVUnitTest/TestSuite/Basics/Arithmetic.hs b/SBVUnitTest/TestSuite/Basics/Arithmetic.hs
deleted file mode 100644
--- a/SBVUnitTest/TestSuite/Basics/Arithmetic.hs
+++ /dev/null
@@ -1,248 +0,0 @@
------------------------------------------------------------------------------
--- |
--- Module      :  TestSuite.Basics.Arithmetic
--- Copyright   :  (c) Levent Erkok
--- License     :  BSD3
--- Maintainer  :  erkokl@gmail.com
--- Stability   :  experimental
---
--- Test suite for basic concrete arithmetic
------------------------------------------------------------------------------
-
-{-# LANGUAGE Rank2Types    #-}
-{-# LANGUAGE TupleSections #-}
-
-module TestSuite.Basics.Arithmetic(testSuite) where
-
-import Data.SBV
-
-import SBVTest
-
--- Test suite
-testSuite :: SBVTestSuite
-testSuite = mkTestSuite $ \_ -> test $
-        genReals
-     ++ genBinTest  "+"                (+)
-     ++ genBinTest  "-"                (-)
-     ++ genBinTest  "*"                (*)
-     ++ genUnTest   "negate"           negate
-     ++ genUnTest   "abs"              abs
-     ++ genUnTest   "signum"           signum
-     ++ genBinTest  ".&."              (.&.)
-     ++ genBinTest  ".|."              (.|.)
-     ++ genBoolTest "<"                (<)  (.<)
-     ++ genBoolTest "<="               (<=) (.<=)
-     ++ genBoolTest ">"                (>)  (.>)
-     ++ genBoolTest ">="               (>=) (.>=)
-     ++ genBoolTest "=="               (==) (.==)
-     ++ genBoolTest "/="               (/=) (./=)
-     ++ genBinTest  "xor"              xor
-     ++ genUnTest   "complement"       complement
-     ++ genIntTest  "shift"            shift
-     ++ genIntTest  "rotate"           rotate
-     ++ genIntTestS "setBit"           setBit
-     ++ genIntTestS "clearBit"         clearBit
-     ++ genIntTestS "complementBit"    complementBit
-     ++ genIntTest  "shift"            shift
-     ++ genIntTestS "shiftL"           shiftL
-     ++ genIntTestS "shiftR"           shiftR
-     ++ genIntTest  "rotate"           rotate
-     ++ genIntTestS "rotateL"          rotateL
-     ++ genIntTestS "rotateR"          rotateR
-     ++ genBlasts
-     ++ genCasts
-
-genBinTest :: String -> (forall a. Bits a => a -> a -> a) -> [Test]
-genBinTest nm op = map mkTest $
-        zipWith pair [(show x, show y, x `op` y) | x <- w8s,  y <- w8s ] [x `op` y | x <- sw8s,  y <- sw8s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `op` y | x <- sw16s, y <- sw16s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `op` y | x <- sw32s, y <- sw32s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `op` y | x <- sw64s, y <- sw64s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s,  y <- i8s ] [x `op` y | x <- si8s,  y <- si8s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `op` y | x <- si16s, y <- si16s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `op` y | x <- si32s, y <- si32s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `op` y | x <- si64s, y <- si64s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `op` y | x <- siUBs, y <- siUBs]
-  where pair (x, y, a) b   = (x, y, show (fromIntegral a `asTypeOf` b) == show b)
-        mkTest (x, y, s) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
-
-genBoolTest :: String -> (forall a. Ord a => a -> a -> Bool) -> (forall a. OrdSymbolic a => a -> a -> SBool) -> [Test]
-genBoolTest nm op opS = map mkTest $
-        zipWith pair [(show x, show y, x `op` y) | x <- w8s,  y <- w8s ] [x `opS` y | x <- sw8s,  y <- sw8s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- w16s, y <- w16s] [x `opS` y | x <- sw16s, y <- sw16s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- w32s, y <- w32s] [x `opS` y | x <- sw32s, y <- sw32s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- w64s, y <- w64s] [x `opS` y | x <- sw64s, y <- sw64s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i8s,  y <- i8s ] [x `opS` y | x <- si8s,  y <- si8s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i16s, y <- i16s] [x `opS` y | x <- si16s, y <- si16s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i32s, y <- i32s] [x `opS` y | x <- si32s, y <- si32s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- i64s, y <- i64s] [x `opS` y | x <- si64s, y <- si64s]
-     ++ zipWith pair [(show x, show y, x `op` y) | x <- iUBs, y <- iUBs] [x `opS` y | x <- siUBs, y <- siUBs]
-  where pair (x, y, a) b   = (x, y, Just a == unliteral b)
-        mkTest (x, y, s) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
-
-genUnTest :: String -> (forall a. Bits a => a -> a) -> [Test]
-genUnTest nm op = map mkTest $
-        zipWith pair [(show x, op x) | x <- w8s ] [op x | x <- sw8s ]
-     ++ zipWith pair [(show x, op x) | x <- w16s] [op x | x <- sw16s]
-     ++ zipWith pair [(show x, op x) | x <- w32s] [op x | x <- sw32s]
-     ++ zipWith pair [(show x, op x) | x <- w64s] [op x | x <- sw64s]
-     ++ zipWith pair [(show x, op x) | x <- i8s ] [op x | x <- si8s ]
-     ++ zipWith pair [(show x, op x) | x <- i16s] [op x | x <- si16s]
-     ++ zipWith pair [(show x, op x) | x <- i32s] [op x | x <- si32s]
-     ++ zipWith pair [(show x, op x) | x <- i64s] [op x | x <- si64s]
-     ++ zipWith pair [(show x, op x) | x <- iUBs] [op x | x <- siUBs]
-  where pair (x, a) b   = (x, show (fromIntegral a `asTypeOf` b) == show b)
-        mkTest (x, s) = "arithmetic-" ++ nm ++ "." ++ x ~: s `showsAs` "True"
-
-genIntTest :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]
-genIntTest nm op = map mkTest $
-        zipWith pair [("u8",  show x, show y, x `op` y) | x <- w8s,  y <- is] [x `op` y | x <- sw8s,  y <- is]
-     ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- is] [x `op` y | x <- sw16s, y <- is]
-     ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- is] [x `op` y | x <- sw32s, y <- is]
-     ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- is] [x `op` y | x <- sw64s, y <- is]
-     ++ zipWith pair [("s8",  show x, show y, x `op` y) | x <- i8s,  y <- is] [x `op` y | x <- si8s,  y <- is]
-     ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- is] [x `op` y | x <- si16s, y <- is]
-     ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- is] [x `op` y | x <- si32s, y <- is]
-     ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- is] [x `op` y | x <- si64s, y <- is]
-     ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- is] [x `op` y | x <- siUBs, y <- is]
-  where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)
-        mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
-        is = [-10 .. 10]
-
-genIntTestS :: String -> (forall a. Bits a => a -> Int -> a) -> [Test]
-genIntTestS nm op = map mkTest $
-        zipWith pair [("u8",  show x, show y, x `op` y) | x <- w8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw8s,  y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("u16", show x, show y, x `op` y) | x <- w16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw16s, y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("u32", show x, show y, x `op` y) | x <- w32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw32s, y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("u64", show x, show y, x `op` y) | x <- w64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- sw64s, y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("s8",  show x, show y, x `op` y) | x <- i8s,  y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si8s,  y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("s16", show x, show y, x `op` y) | x <- i16s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si16s, y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("s32", show x, show y, x `op` y) | x <- i32s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si32s, y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("s64", show x, show y, x `op` y) | x <- i64s, y <- [0 .. (bitSize x - 1)]] [x `op` y | x <- si64s, y <- [0 .. (bitSize x - 1)]]
-     ++ zipWith pair [("iUB", show x, show y, x `op` y) | x <- iUBs, y <- [0 .. 10]]              [x `op` y | x <- siUBs, y <- [0 .. 10             ]]
-  where pair (t, x, y, a) b       = (t, x, y, show a, show b, show (fromIntegral a `asTypeOf` b) == show b)
-        mkTest (t, x, y, a, b, s) = "arithmetic-" ++ nm ++ "." ++ t ++ "_" ++ x ++ "_" ++ y ++ "_" ++ a ++ "_" ++ b ~: s `showsAs` "True"
-
-genBlasts :: [Test]
-genBlasts = map mkTest $
-             [(show x, fromBitsLE (blastLE x) .== x) | x <- sw8s ]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw8s ]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si8s ]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si8s ]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw16s]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw16s]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si16s]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si16s]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw32s]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw32s]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si32s]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si32s]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- sw64s]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- sw64s]
-          ++ [(show x, fromBitsLE (blastLE x) .== x) | x <- si64s]
-          ++ [(show x, fromBitsBE (blastBE x) .== x) | x <- si64s]
-  where mkTest (x, r) = "blast-" ++ show x ~: r `showsAs` "True"
-
-genCasts :: [Test]
-genCasts = map mkTest $
-            [(show x, unsignCast (signCast x) .== x) | x <- sw8s ]
-         ++ [(show x, unsignCast (signCast x) .== x) | x <- sw16s]
-         ++ [(show x, unsignCast (signCast x) .== x) | x <- sw32s]
-         ++ [(show x, unsignCast (signCast x) .== x) | x <- sw64s]
-         ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]
-         ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]
-         ++ [(show x, signCast (unsignCast x) .== x) | x <- si8s ]
-         ++ [(show x, signCast (unsignCast x) .== x) | x <- si16s]
-         ++ [(show x, signCast (unsignCast x) .== x) | x <- si32s]
-         ++ [(show x, signCast (unsignCast x) .== x) | x <- si64s]
-         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw8s ]
-         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw16s]
-         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw32s]
-         ++ [(show x, signCast x .== fromBitsLE (blastLE x))   | x <- sw64s]
-         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si8s ]
-         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si16s]
-         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si32s]
-         ++ [(show x, unsignCast x .== fromBitsLE (blastLE x)) | x <- si64s]
-  where mkTest (x, r) = "cast-" ++ show x ~: r `showsAs` "True"
-
-genReals :: [Test]
-genReals = map mkTest $
-        map ("+",)  (zipWith pair [(show x, show y, x +  y) | x <- rs, y <- rs        ] [x +   y | x <- srs,  y <- srs                       ])
-     ++ map ("-",)  (zipWith pair [(show x, show y, x -  y) | x <- rs, y <- rs        ] [x -   y | x <- srs,  y <- srs                       ])
-     ++ map ("*",)  (zipWith pair [(show x, show y, x *  y) | x <- rs, y <- rs        ] [x *   y | x <- srs,  y <- srs                       ])
-     ++ map ("<",)  (zipWith pair [(show x, show y, x <  y) | x <- rs, y <- rs        ] [x .<  y | x <- srs,  y <- srs                       ])
-     ++ map ("<=",) (zipWith pair [(show x, show y, x <= y) | x <- rs, y <- rs        ] [x .<= y | x <- srs,  y <- srs                       ])
-     ++ map (">",)  (zipWith pair [(show x, show y, x >  y) | x <- rs, y <- rs        ] [x .>  y | x <- srs,  y <- srs                       ])
-     ++ map (">=",) (zipWith pair [(show x, show y, x >= y) | x <- rs, y <- rs        ] [x .>= y | x <- srs,  y <- srs                       ])
-     ++ map ("==",) (zipWith pair [(show x, show y, x == y) | x <- rs, y <- rs        ] [x .== y | x <- srs,  y <- srs                       ])
-     ++ map ("/=",) (zipWith pair [(show x, show y, x /= y) | x <- rs, y <- rs        ] [x ./= y | x <- srs,  y <- srs                       ])
-     ++ map ("/",)  (zipWith pair [(show x, show y, x /  y) | x <- rs, y <- rs, y /= 0] [x / y   | x <- srs,  y <- srs, unliteral y /= Just 0])
-  where pair (x, y, a) b   = (x, y, Just a == unliteral b)
-        mkTest (nm, (x, y, s)) = "arithmetic-" ++ nm ++ "." ++ x ++ "_" ++ y  ~: s `showsAs` "True"
-
--- Concrete test data
-xsSigned, xsUnsigned :: (Num a, Enum a, Bounded a) => [a]
-xsUnsigned = take 5 (iterate (1+) minBound) ++ take 5 (iterate (\x -> x-1) maxBound)
-xsSigned   = xsUnsigned ++ [-5 .. 5]
-
-w8s :: [Word8]
-w8s = xsUnsigned
-
-sw8s :: [SWord8]
-sw8s = xsUnsigned
-
-w16s :: [Word16]
-w16s = xsUnsigned
-
-sw16s :: [SWord16]
-sw16s = xsUnsigned
-
-w32s :: [Word32]
-w32s = xsUnsigned
-
-sw32s :: [SWord32]
-sw32s = xsUnsigned
-
-w64s :: [Word64]
-w64s = xsUnsigned
-
-sw64s :: [SWord64]
-sw64s = xsUnsigned
-
-i8s :: [Int8]
-i8s = xsSigned
-
-si8s :: [SInt8]
-si8s = xsSigned
-
-i16s :: [Int16]
-i16s = xsSigned
-
-si16s :: [SInt16]
-si16s = xsSigned
-
-i32s :: [Int32]
-i32s = xsSigned
-
-si32s :: [SInt32]
-si32s = xsSigned
-
-i64s :: [Int64]
-i64s = xsSigned
-
-si64s :: [SInt64]
-si64s = xsSigned
-
-iUBs :: [Integer]
-iUBs = [-1000000 .. -999995] ++ [-5 .. 5] ++ [999995 ..  1000000]
-
-siUBs :: [SInteger]
-siUBs = map literal iUBs
-
-rs :: [AlgReal]
-rs = [fromRational (i % d) | i <- is, d <- ds]
- where is = [-1000000 .. -999998] ++ [-2 .. 2] ++ [999998 ..  1000001]
-       ds = [2 .. 5] ++ [98 .. 102] ++ [999998 .. 1000000]
-
-srs :: [SReal]
-srs = map literal rs
diff --git a/SBVUnitTest/TestSuite/Basics/QRem.hs b/SBVUnitTest/TestSuite/Basics/QRem.hs
--- a/SBVUnitTest/TestSuite/Basics/QRem.hs
+++ b/SBVUnitTest/TestSuite/Basics/QRem.hs
@@ -19,5 +19,7 @@
 -- Test suite
 testSuite :: SBVTestSuite
 testSuite = mkTestSuite $ \_ -> test [
-   "qrem" ~: assert =<< isTheorem (qrem :: SWord8 -> SWord8 -> SBool)
+   "qremW8" ~: assert =<< isTheorem (qrem :: SWord8   -> SWord8   -> SBool)
+ , "qremI8" ~: assert =<< isTheorem (qrem :: SInt8    -> SInt8    -> SBool)
+ , "qremI"  ~: assert =<< isTheorem (qrem :: SInteger -> SInteger -> SBool)
  ]
diff --git a/SBVUnitTest/TestSuite/Puzzles/Temperature.hs b/SBVUnitTest/TestSuite/Puzzles/Temperature.hs
--- a/SBVUnitTest/TestSuite/Puzzles/Temperature.hs
+++ b/SBVUnitTest/TestSuite/Puzzles/Temperature.hs
@@ -19,5 +19,5 @@
 -- Test suite
 testSuite :: SBVTestSuite
 testSuite = mkTestSuite $ \goldCheck -> test [
-  "temperature" ~: sat (revOf `fmap` exists_) `goldCheck` "temperature.gold"
+  "temperature" ~: allSat (revOf `fmap` exists_) `goldCheck` "temperature.gold"
  ]
diff --git a/sbv.cabal b/sbv.cabal
--- a/sbv.cabal
+++ b/sbv.cabal
@@ -1,5 +1,5 @@
 Name:          sbv
-Version:       2.3
+Version:       2.4
 Category:      Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
 Synopsis:      SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
 Description:   Express properties about Haskell programs and automatically prove them using SMT
@@ -15,8 +15,10 @@
                >   Falsifiable. Counter-example:
                >     x = 128 :: SWord8
                .
-               The library introduces the following types and concepts:
+               The SBV library uses Microsoft's Z3 SMT solver (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>) as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (<http://yices.csl.sri.com/download-yices2.shtml>), although the Z3 binding is much more richer.
                .
+               SBV introduces the following types and concepts:
+               .
                  * 'SBool': Symbolic Booleans (bits)
                .
                  * 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned)
@@ -115,22 +117,8 @@
                     TypeOperators
                     TypeSynonymInstances
   Build-Depends   : base >= 4 && < 5
-                  -- Be careful with versions of packages that come with "latest" GHC,
-                  -- need to update this as new GHC releases incorporate new packages
-                  , array               == 0.4.0.0
-                  , containers          == 0.4.2.1
-                  , deepseq             == 1.3.0.0
-                  , directory           == 1.1.0.2
-                  , filepath            == 1.3.0.0
-                  , old-time            == 1.1.0.0
-                  , pretty              == 1.1.1.0
-                  , process             == 1.1.0.1
-                  -- following are pure hackage packages, thus we can be more relaxed
-                  , mtl                 >= 2.1.2
-                  , QuickCheck          >= 2.5
-                  , random              >= 1.0.1.1
-                  , strict-concurrency  >= 0.2.4.1
-                  , syb                 >= 0.3.7
+                  , array, containers, deepseq, directory, filepath, old-time
+                  , pretty, process, mtl, QuickCheck, random, strict-concurrency, syb
   Exposed-modules : Data.SBV
                   , Data.SBV.Internals
                   , Data.SBV.Examples.BitPrecise.BitTricks
@@ -192,20 +180,13 @@
                     RankNTypes
                     ScopedTypeVariables
                     TupleSections
-  Build-depends   : base >= 4 && < 5
-                  -- Be careful with versions of packages that come with "latest" GHC,
-                  -- need to update this as new GHC releases incorporate new packages
-                  , directory == 1.1.0.2
-                  , filepath  == 1.3.0.0
-                  , process   == 1.1.0.1
-                  -- apparently HUnit 1.2.5.0 has some cabal issues..
-                  , HUnit     == 1.2.4.3
-                  -- self dependence on sbv
-                  , sbv
+  Build-depends   : base  >= 4 && < 5
+                  , HUnit, directory, filepath, process, sbv
   Hs-Source-Dirs  : SBVUnitTest
   main-is         : SBVUnitTest.hs
   Other-modules   : SBVUnitTestBuildTime
                   , SBVTest
+                  , SBVTestCollection
                   , Examples.Arrays.Memory
                   , Examples.Basics.BasicTests
                   , Examples.Basics.Higher
@@ -221,7 +202,8 @@
                   , Examples.Puzzles.Temperature
                   , Examples.Uninterpreted.Uninterpreted
                   , TestSuite.Arrays.Memory
-                  , TestSuite.Basics.Arithmetic
+                  , TestSuite.Basics.ArithNoSolver
+                  , TestSuite.Basics.ArithSolver
                   , TestSuite.Basics.BasicTests
                   , TestSuite.Basics.Higher
                   , TestSuite.Basics.Index
@@ -260,3 +242,14 @@
                   , TestSuite.Uninterpreted.AUF
                   , TestSuite.Uninterpreted.Function
                   , TestSuite.Uninterpreted.Uninterpreted
+
+Test-Suite SBVBasicTests
+  type            : exitcode-stdio-1.0
+  default-language: Haskell2010
+  ghc-options     : -Wall
+  Build-depends   : base >= 4 && < 5
+                  , HUnit, directory, filepath, sbv
+  Hs-Source-Dirs  : SBVUnitTest
+  main-is         : SBVBasicTests.hs
+  Other-modules   : SBVBasicTests
+                  , SBVTestCollection