aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/Z3Interface.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/Z3Interface.cpp')
-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)