diff --git a/src/solvers/sat/satcheck_minisat2.cpp b/src/solvers/sat/satcheck_minisat2.cpp
index 1cd70665814..fe9ed4527ca 100644
--- a/src/solvers/sat/satcheck_minisat2.cpp
+++ b/src/solvers/sat/satcheck_minisat2.cpp
@@ -155,7 +155,7 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
         {
           messaget::status() <<
             "SAT checker: instance is SATISFIABLE" << eom;
-          assert(!solver->model.empty());
+          CHECK_RETURN(solver->model.size()>0);
           status=statust::SAT;
           return resultt::P_SATISFIABLE;
         }
diff --git a/src/util/graph.h b/src/util/graph.h
index 4a49719f7a2..6ef7976ad0a 100644
--- a/src/util/graph.h
+++ b/src/util/graph.h
@@ -150,6 +150,11 @@ class grapht
     return nodes.size();
   }
 
+  bool empty() const
+  {
+    return nodes.empty();
+  }
+
   const edgest &in(node_indext n) const
   {
     return nodes[n].in;