Correctly handle SMT solver errors

`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,10 @@ 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)();
+  if(result == decision_proceduret::resultt::D_ERROR)
+    throw "error running the SMT solver";
+  return (result == decision_proceduret::resultt::D_SATISFIABLE);
 }
 
 exprt scratch_programt::eval(const exprt &e)