diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 21ca6037bbe6f1050e70a867ad4e2252e0dc3069..0f967af9d72de489e4cdaf0d409241925679f272 100644
--- a/src/SimpleFormulaChecker.hs
+++ b/src/SimpleFormulaChecker.hs
@@ -187,7 +187,7 @@ determineFormulaEq m1@(decls1, mbody1, env1) m2@(decls2, mbody2, env2) name = do
        Sat   -> do
                 putStrLn "formulas are NOT equivalent, model:"
                 case model of
-                  Just m -> do s <- evalZ3 (modelToString m)
+                  Just m -> do s <- evalZ3With Nothing (Z3.Opts.opt "timeout" (1000 :: Int)) (modelToString m) -- TODO: the option is set, but does not actually work :(
                                putStrLn $ "Raw model:\n" ++ s
                                showRelevantModel $ parseModel s
                   _      -> return ()