Throw exception when IC3 bad state reachability check result is unkno…

…wn (#352)

Currently, if the invoked SMT solver returns "unknown," we fail an assertion in debug mode and silently proceed as if it was unsat in release mode. This can happen on e.g. Bitwuzla when there are equalities involving constant arrays. (Other solvers might do this too, although some simply return incorrect results.)

engines/ic3base.cpp

@@ -17,10 +17,11 @@
 
 #include "engines/ic3base.h"
 
-#include "assert.h"
+#include <cassert>
+
 #include "smt/available_solvers.h"
+#include "utils/exceptions.h"
 #include "utils/logger.h"
-#include "utils/term_analysis.h"
 
 using namespace smt;
 using namespace std;
@@ -366,7 +367,10 @@ bool IC3Base::reaches_bad(IC3Formula & out)
 
   pop_solver_context();
 
-  assert(!r.is_unknown());
+  if (r.is_unknown()) {
+    throw PonoException("Bad state check in IC3 returned unknown");
+  }
+
   return r.is_sat();
 }
 
@@ -648,7 +652,7 @@ bool IC3Base::block_all()
     }  // end while(!proof_goals.empty())
 
     assert(!(goal = IC3Formula()).term);  // in debug mode, reset it
-  }                                       // end while(reaches_bad(goal))
+  }  // end while(reaches_bad(goal))
 
   assert(proof_goals.empty());
   return true;