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.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index 6111b2c8..0c083abc 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -91,7 +91,7 @@ pair<CheckResult, vector<string>> Z3Interface::check(vector<Expression> const& _
solAssert(false, "");
}
- if (result != CheckResult::UNSATISFIABLE)
+ if (result != CheckResult::UNSATISFIABLE && !_expressionsToEvaluate.empty())
{
z3::model m = m_solver.get_model();
for (Expression const& e: _expressionsToEvaluate)