aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-10-04 20:56:24 +0800
committerGitHub <noreply@github.com>2017-10-04 20:56:24 +0800
commitf6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78 (patch)
tree7816b6b544ea0794032deed0f14e15f0dfc8057b /libsolidity
parent22f112fc13e8d609435e53e18a66d0b0664b5c44 (diff)
parentfefdfc0711e1637df91ef0ec813af0c30ad53af6 (diff)
downloaddexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.tar
dexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.tar.gz
dexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.tar.bz2
dexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.tar.lz
dexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.tar.xz
dexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.tar.zst
dexon-solidity-f6fb7d96d3eb0d45ee93fbe25f01cb9f06b28b78.zip
Merge pull request #2990 from ethereum/someMoreSMTStuff
Basic SMT tests.
Diffstat (limited to 'libsolidity')
-rw-r--r--libsolidity/formal/Z3Interface.cpp7
1 files changed, 0 insertions, 7 deletions
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 522928f0..fbbd7a58 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -72,28 +72,21 @@ void Z3Interface::addAssertion(Expression const& _expr)
pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _expressionsToEvaluate)
{
-// cout << "---------------------------------" << endl;
-// cout << m_solver << endl;
CheckResult result;
switch (m_solver.check())
{
case z3::check_result::sat:
result = CheckResult::SATISFIABLE;
- cout << "sat" << endl;
break;
case z3::check_result::unsat:
result = CheckResult::UNSATISFIABLE;
- cout << "unsat" << endl;
break;
case z3::check_result::unknown:
result = CheckResult::UNKNOWN;
- cout << "unknown" << endl;
break;
default:
solAssert(false, "");
}
-// cout << "---------------------------------" << endl;
-
vector<string> values;
if (result != CheckResult::UNSATISFIABLE)