Skip to content
Snippets Groups Projects
Verified Commit 01706067 authored by Ogilvie, D.H. (Duncan)'s avatar Ogilvie, D.H. (Duncan)
Browse files

set timeout option

does not actually work though
parent 205f0337
No related branches found
No related tags found
No related merge requests found
......@@ -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 ()
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment