Do not ignore SMT solver failures

`check_sat` in scratch_programt was treating UNSAT and ERROR as the same. This was causing SMT solver errors to be silently ignored, and be treated as UNSAT results instead.

Author: SaswatPadhi

src/goto-instrument/accelerate/scratch_program.cpp

@@ -71,7 +71,12 @@ bool scratch_programt::check_sat(bool do_slice, guard_managert &guard_manager)
   std::cout << "Finished symex, invoking decision procedure.\n";
 #endif
 
-  return ((*checker)() == decision_proceduret::resultt::D_SATISFIABLE);
+  auto result = (*checker)();
+  INVARIANT(
+    result != decision_proceduret::resultt::D_ERROR,
+    "Error running the SMT solver");
+
+  return (result == decision_proceduret::resultt::D_SATISFIABLE);
 }
 
 exprt scratch_programt::eval(const exprt &e)