From 01706067aed5071142c4d7137db9327ab1ebbc8e Mon Sep 17 00:00:00 2001
From: Duncan Ogilvie <mr.exodia.tpodt@gmail.com>
Date: Sat, 18 Nov 2017 15:01:49 +0100
Subject: [PATCH] set timeout option
does not actually work though
---
src/SimpleFormulaChecker.hs | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/src/SimpleFormulaChecker.hs b/src/SimpleFormulaChecker.hs
index 21ca603..0f967af 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 ()
--
GitLab