cerc-io/solidity
15
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

Merge pull request #4593 from ethereum/smt_timeout

Browse Source 
Set query timeout in SMT
This commit is contained in:
Alex Beregszaszi 2018-07-27 15:42:55 +01:00 committed by GitHub
commit 5faa60e883
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
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_solver.reset();
m_solver.setOption("produce-models", true);
m_solver.setTimeLimit(queryTimeout);
}
void CVC4Interface::push()

5
libsolidity/formal/SolverInterface.h
View File

@ -231,9 +231,12 @@ public:
/// is available. Throws SMTSolverError on error.
virtual std::pair<CheckResult, std::vector<std::string>>
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():
m_solver(m_context)
{
// This needs to be set globally.
z3::set_param("rewriter.pull_cheap_ite", true);
// This needs to be set in the context.
m_context.set("timeout", queryTimeout);
}
void Z3Interface::reset()