Ignore quantifier errors running get-value commands with z3

Due to how we call z3 it is possible to have values that contain
quantifiers appear in the results. However, z3 cannot give a
real value in response to a "(get-value |XXX|)" request.
This catches these any simply ignores them, allowing the rest
of the code to continue.

Note that this becomes necessary to handle since cbmc now
produces quantifiers in expressions sent to z3.

Author: thomasspriggs

src/solvers/smt2/smt2_dec.cpp

@@ -175,17 +175,36 @@ decision_proceduret::resultt smt2_dect::read_result(std::istream &in)
     {
       // We ignore errors after UNSAT because get-value after check-sat
       // returns unsat will give an error.
-      if(res!=resultt::D_UNSATISFIABLE)
+      if(res != resultt::D_UNSATISFIABLE)
       {
-        messaget log{message_handler};
-        log.error() << "SMT2 solver returned error message:\n"
-                    << "\t\"" << parsed.get_sub()[1].id() << "\""
-                    << messaget::eom;
-        return decision_proceduret::resultt::D_ERROR;
+        const auto &message = id2string(parsed.get_sub()[1].id());
+        // Special case error handling
+        if(
+          solver == solvert::Z3 &&
+          message.find("must not contain quantifiers") != std::string::npos)
+        {
+          // We tried to "(get-value |XXXX|)" where |XXXX| is determined to
+          // include a quantified expression
+          // Nothing to do, this should be caught and value assigned by the
+          // set_to defaults later.
+        }
+        // Unhandled error, log the error and report it back up to caller
+        else
+        {
+          messaget log{message_handler};
+          log.error() << "SMT2 solver returned error message:\n"
+                      << "\t\"" << message << "\"" << messaget::eom;
+          return decision_proceduret::resultt::D_ERROR;
+        }
       }
     }
   }
 
+  // If the result is satisfiable don't bother updating the assignments and
+  // values (since we didn't get any), just return.
+  if(res != resultt::D_SATISFIABLE)
+    return res;
+
   for(auto &assignment : identifier_map)
   {
     std::string conv_id=convert_identifier(assignment.first);