cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

Setting timeout to Z3 and CVC4

Browse Source
This commit is contained in:
Leonardo Alt 2018-07-27 09:14:50 +02:00
parent c633ebe2e6
commit b356f6a7f9
3 changed files with 8 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
libsolidity/formal/CVC4Interface.cpp
View File

@ -37,6 +37,7 @@ void CVC4Interface::reset()
m_functions.clear(); m_functions.clear();
m_solver.reset(); m_solver.reset();
m_solver.setOption("produce-models", true); m_solver.setOption("produce-models", true);
m_solver.setTimeLimit(queryTimeout);
} }
void CVC4Interface::push() void CVC4Interface::push()

5
libsolidity/formal/SolverInterface.h
View File

@ -231,9 +231,12 @@ public:
/// is available. Throws SMTSolverError on error. /// is available. Throws SMTSolverError on error.
virtual std::pair<CheckResult, std::vector<std::string>> virtual std::pair<CheckResult, std::vector<std::string>>
check(std::vector<Expression> const& _expressionsToEvaluate) = 0; check(std::vector<Expression> const& _expressionsToEvaluate) = 0;
protected:
// SMT query timeout in milliseconds.
static int const queryTimeout = 10000;
}; };
} }
} }
} }

3
libsolidity/formal/Z3Interface.cpp
View File

@ -28,7 +28,10 @@ using namespace dev::solidity::smt;
Z3Interface::Z3Interface(): Z3Interface::Z3Interface():
m_solver(m_context) m_solver(m_context)
{ {
// This needs to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true); z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context.
m_context.set("timeout", queryTimeout);
} }
void Z3Interface::reset() void Z3Interface::reset()