Add lookup for non-lowered exprt in get_identifier

This fixes a problem with looking up the value of an assertion, which
resulted in the properties not being properly updated after the
property decider had run.
This was because assertion expressions are given a handle symbol that is
queried to the solver. The decision procedure was trying to resolve the
handle from a lowered expression and not the original that was saved in
the map not receiving the correct symbol back.

Author: Enrico Steffinlongo

src/solvers/smt2_incremental/smt2_incremental_decision_procedure.cpp

@@ -351,14 +351,24 @@ static optionalt<smt_termt> get_identifier(
     &expression_identifiers,
   const namespacet &ns)
 {
-  const exprt lowered_expr = lower_enum(expr, ns);
-  const auto handle_find_result =
-    expression_handle_identifiers.find(lowered_expr);
+  // Lookup the non-lowered form first.
+  const auto handle_find_result = expression_handle_identifiers.find(expr);
   if(handle_find_result != expression_handle_identifiers.cend())
     return handle_find_result->second;
-  const auto expr_find_result = expression_identifiers.find(lowered_expr);
+  const auto expr_find_result = expression_identifiers.find(expr);
   if(expr_find_result != expression_identifiers.cend())
     return expr_find_result->second;
+
+  // If that didn't yield any results, then try the lowered form.
+  const exprt lowered_expr = lower_enum(expr, ns);
+  const auto lowered_handle_find_result =
+    expression_handle_identifiers.find(lowered_expr);
+  if(lowered_handle_find_result != expression_handle_identifiers.cend())
+    return lowered_handle_find_result->second;
+  const auto lowered_expr_find_result =
+    expression_identifiers.find(lowered_expr);
+  if(lowered_expr_find_result != expression_identifiers.cend())
+    return lowered_expr_find_result->second;
   return {};
 }