diff --git a/hylolib.cabal b/hylolib.cabal
--- a/hylolib.cabal
+++ b/hylolib.cabal
@@ -1,5 +1,5 @@
 Name:                hylolib
-Version:             1.3.0
+Version:             1.3.1
 Synopsis:            Tools for hybrid logics related programs
 License:             GPL
 License-file:        LICENSE
@@ -8,6 +8,8 @@
 Build-Type:          Simple
 Cabal-Version:       >= 1.2.3
 Category:            Theorem Provers
+
+Extra-source-files:  unit-tests/hylolib-testsuite.hs
 
 Library
   Build-Depends:       base >= 4, base < 5,
diff --git a/src/HyLo/InputFile.hs b/src/HyLo/InputFile.hs
--- a/src/HyLo/InputFile.hs
+++ b/src/HyLo/InputFile.hs
@@ -1,4 +1,4 @@
-module HyLo.InputFile ( InputFile, parse, myparse, write, parseOldFormat,
+module HyLo.InputFile ( InputFile, parse, myparse, write, parseOldFormat, OldInputFile,
                         --unit_tests
                         )
 
@@ -34,7 +34,7 @@
 myparse :: String -> P.ParseOutput
 myparse = runParser . P.parse . L.lexify
 
-write :: InputFile -> String
+write :: (Show n, Show p, Show r) => [Formula n p r] -> String
 write input = unlines $ "{":addSemicolon (map show input) ++ ["}"]
     where addSemicolon (x:xs@(_:_)) = (x ++ ";") : addSemicolon xs
           addSemicolon xs           = xs
diff --git a/src/HyLo/Model.hs b/src/HyLo/Model.hs
--- a/src/HyLo/Model.hs
+++ b/src/HyLo/Model.hs
@@ -1,6 +1,6 @@
 module HyLo.Model ( Model, worlds, succs, valP, valN,
                     model, equiv, expand, setSignature, (??),
-                    removeWorld, removeWorlds,
+                    removeWorld, removeWorlds, countInModel,
                     namesOf, propsOf,
                     ModelsRel(..), (|/=),
                     --
@@ -250,6 +250,9 @@
 propsOf :: Ord w => w -> Model w n p r -> [p]
 propsOf w m = [p | p <- toList . propSymbols . getSignature $ m,
                    w `Set.member` valP m p]
+
+countInModel :: (Ord w, Ord n, Ord p, Ord r) => F.Formula n p r -> Model w n p r -> Int
+countInModel f m = length [ w | w <- toList (worlds m), (m,w) |= f ]
 
 -- -----------------------------
 -- QuickCheck stuff
diff --git a/unit-tests/hylolib-testsuite.hs b/unit-tests/hylolib-testsuite.hs
new file mode 100644
--- /dev/null
+++ b/unit-tests/hylolib-testsuite.hs
@@ -0,0 +1,30 @@
+module Main ( main )
+
+where
+
+import Control.Monad ( when )
+import System.Exit   ( exitFailure )
+
+import HyLo.Test ( TestResult(OK), UnitTest, ModuleName,
+                   stopOnError, testSuite )
+
+import qualified HyLo.Signature        ( unit_tests )
+import qualified HyLo.Signature.Simple ( unit_tests )
+import qualified HyLo.Formula          ( unit_tests )
+import qualified HyLo.Model            ( unit_tests )
+import qualified HyLo.Model.Herbrand   ( unit_tests )
+
+all_tests :: [(ModuleName, UnitTest)]
+all_tests = [
+    ("HyLo.Signature",        HyLo.Signature.unit_tests),
+    ("HyLo.Signature.Simple", HyLo.Signature.Simple.unit_tests),
+    ("HyLo.Formula",          HyLo.Formula.unit_tests),
+    ("HyLo.Model",            HyLo.Model.unit_tests),
+    ("HyLo.Model.Herbrand",   HyLo.Model.Herbrand.unit_tests)
+  ]
+
+main :: IO ()
+main = do rs <- stopOnError testSuite all_tests
+          when (not $ all (== OK) rs) $ do
+               putStrLn "Some tests did not pass!"
+               exitFailure