diff options
| author | chriseth <chris@ethereum.org> | 2017-08-21 23:02:47 +0800 |
|---|---|---|
| committer | chriseth <chris@ethereum.org> | 2017-08-23 23:37:35 +0800 |
| commit | cf5e1d6120513c757bd5c71f1e3af972a9a63aeb (patch) | |
| tree | 6910848eb79274896826e69a603e8a34fb5fadc3 /libsolidity/formal/Z3Interface.cpp | |
| parent | 8853183d060104777b03921ccda1e9db600f0e8e (diff) | |
| download | dexon-solidity-cf5e1d6120513c757bd5c71f1e3af972a9a63aeb.tar.gz dexon-solidity-cf5e1d6120513c757bd5c71f1e3af972a9a63aeb.tar.zst dexon-solidity-cf5e1d6120513c757bd5c71f1e3af972a9a63aeb.zip | |
Review changes.
Diffstat (limited to 'libsolidity/formal/Z3Interface.cpp')
| -rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index bb0d6f6f..522928f0 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -78,11 +78,11 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _ switch (m_solver.check()) { case z3::check_result::sat: - result = CheckResult::SAT; + result = CheckResult::SATISFIABLE; cout << "sat" << endl; break; case z3::check_result::unsat: - result = CheckResult::UNSAT; + result = CheckResult::UNSATISFIABLE; cout << "unsat" << endl; break; case z3::check_result::unknown: @@ -96,7 +96,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _ vector<string> values; - if (result != CheckResult::UNSAT) + if (result != CheckResult::UNSATISFIABLE) { z3::model m = m_solver.get_model(); for (Expression const& e: _expressionsToEvaluate) |