Fix test suite and include test for issue #5

test/Spec.hs

@@ -1 +1,11 @@
-{-# OPTIONS_GHC -F -pgmF hspec-discover #-}
+
+import Test.Hspec
+
+import qualified Z3.Base.Spec
+
+main :: IO ()
+main = hspec spec
+
+spec :: Spec
+spec = do
+  describe "Z3.Base" Z3.Base.Spec.spec

test/Z3/Base/Spec.hs

@@ -15,6 +15,9 @@ withContext k = do
   ctx <- Z3.withConfig Z3.mkContext
   k ctx
 
+anyZ3Error :: Selector Z3.Z3Error
+anyZ3Error = const True
+
 spec :: Spec
 spec = around withContext $ do
 
@@ -24,14 +27,23 @@ spec = around withContext $ do
       monadicIO $ do
         x::Maybe Bool <- run $ do
           ast <- Z3.mkBool ctx b
-          Z3.getBool ctx ast
+          Z3.getBoolValue ctx ast
         assert $ x == Just b
 
   context "Numerals" $ do
 
     specify "mkInt" $ \ctx -> property $ \(i :: Integer) ->
       monadicIO $ do
         x::Integer <- run $ do
-          ast <- Z3.mkInt ctx i;
+          ast <- Z3.mkInteger ctx i;
           Z3.getInt ctx ast;
-        assert $ x == i
+        assert $ x == i
+
+  context "Bit-vectors" $ do
+
+    specify "mkBvmul" $ \ctx ->
+      let bad = do
+          x <- Z3.mkFreshIntVar ctx "x";
+          Z3.mkBvmul ctx x x
+      in bad `shouldThrow` anyZ3Error
+

z3.cabal

@@ -110,6 +110,8 @@ Test-suite spec
 
     Main-is:            Spec.hs
 
+    Other-modules:      Z3.Base.Spec
+
     Build-depends:      base >= 4.5,
                         z3 == 4.*,
                         hspec >= 2.1,