Merge pull request #1040 from tautschnig/fix-1032

Daniel Kroening · web-flow · commit 7dbb20313a51 · 2017-06-19T21:14:36.000+01:00
Add empty() to grapht as it implements size()
diff --git 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
@@ -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;

Original file line number	Diff line number	Diff line change
`@@ -155,7 +155,7 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()`
`155`	`155`	`{`
`156`	`156`	`messaget::status() <<`
`157`	`157`	`"SAT checker: instance is SATISFIABLE" << eom;`
`158`		`- assert(!solver->model.empty());`
	`158`	`+ CHECK_RETURN(solver->model.size()>0);`
`159`	`159`	`status=statust::SAT;`
`160`	`160`	`return resultt::P_SATISFIABLE;`
`161`	`161`	`}`
Original file line number	Diff line number	Diff line change
`@@ -150,6 +150,11 @@ class grapht`
`150`	`150`	`return nodes.size();`
`151`	`151`	`}`
`152`	`152`
	`153`	`+ bool empty() const`
	`154`	`+ {`
	`155`	`+ return nodes.empty();`
	`156`	`+ }`
	`157`	`+`
`153`	`158`	`const edgest &in(node_indext n) const`
`154`	`159`	`{`
`155`	`160`	`return nodes[n].in;`