bump CBMC

src/fastsynth/bool_synth_encoding.cpp

@@ -385,7 +385,7 @@ bool_e_datat::bool_e_datat(
   const std::size_t program_size)
   : function_arguments(expression.arguments())
 {
-  function_symbol = expression.function();
+  function_symbol = to_symbol_expr(expression.function());
   const irep_idt &identifier = function_symbol.get_identifier();
 
   PRECONDITION(is_bool_word_type());
@@ -413,13 +413,14 @@ exprt bool_synth_encodingt::operator()(const exprt &expr)
     for(exprt &op : function_expr.arguments())
       op = (*this)(op);
 
-    auto map_it = e_data_per_function.find(function_expr.function());
+    auto map_it = e_data_per_function.find(
+        to_symbol_expr(function_expr.function()));
     if(map_it == end(e_data_per_function))
     {
       bool_e_datat new_data{function_expr, program_size};
       new_data.literals = literals;
       map_it = e_data_per_function
-                 .emplace(function_expr.function(), std::move(new_data))
+                 .emplace(to_symbol_expr(function_expr.function()), std::move(new_data))
                  .first;
     }
     bool_e_datat &e_data = map_it->second;

src/fastsynth/local_synth_encoding.cpp

@@ -117,7 +117,8 @@ exprt local_synth_encodingt::operator()(const exprt &expr)
       actual_params.emplace(placeholder, (*this)(op));
     }
 
-    const irep_idt &identifier = func->function().get_identifier();
+    const irep_idt &identifier =
+        to_symbol_expr(func->function()).get_identifier();
     const std::map<symbol_exprt, exprt>::const_iterator it = find_if(
       begin(solution_template.functions),
       end(solution_template.functions),

src/fastsynth/sygus_parser.cpp

@@ -1044,7 +1044,7 @@ void sygus_parsert::expand_function_applications(exprt &expr)
     auto &app=to_function_application_expr(expr);
 
     // look it up
-    irep_idt identifier=app.function().get_identifier();
+    irep_idt identifier=to_symbol_expr(app.function()).get_identifier();
     auto f_it=function_map.find(identifier);
 
     if(f_it!=function_map.end())
@@ -1053,7 +1053,8 @@ void sygus_parsert::expand_function_applications(exprt &expr)
 
       if(synth_fun_set.find(identifier)!=synth_fun_set.end())
       {
-        app.function().set_identifier("synth_fun::"+id2string(identifier));
+        to_symbol_expr(app.function()).set_identifier
+            ("synth_fun::"+id2string(identifier));
         return; // do not expand
       }
 

src/fastsynth/synth_encoding.cpp

@@ -66,7 +66,7 @@ void e_datat::setup(
 
   enable_bitwise=_enable_bitwise;
 
-  function_symbol=e.function();
+  function_symbol=to_symbol_expr(e.function());
   const irep_idt &identifier=function_symbol.get_identifier();
 
   return_type=e.type();
@@ -551,10 +551,11 @@ exprt synth_encodingt::operator()(const exprt &expr)
     for(auto &op : tmp.arguments())
       op=(*this)(op);
 
-    e_datat &e_data=e_data_map[tmp.function()];
+    e_datat &e_data=e_data_map[to_symbol_expr(tmp.function())];
     if(e_data.word_type.id().empty())
       e_data.literals=literals;
-    exprt final_result=e_data(tmp, program_size, enable_bitwise, enable_division);
+    exprt final_result=e_data(
+        tmp, program_size, enable_bitwise, enable_division);
 
     for(const auto &c : e_data.constraints)
       constraints.push_back(c);

src/fastsynth/verify_encoding.cpp

@@ -81,7 +81,9 @@ exprt verify_encodingt::operator()(const exprt &expr) const
     for(const auto &f : functions)
       f_map[f.first.get_identifier()]=f.second;
 
-    auto f_it=f_map.find(e.function().get_identifier());
+    auto f_it=f_map.find(to_symbol_expr(e.function()).get_identifier());
+
+
 
     exprt result=f_it==f_map.end()?
       from_integer(0, e.type()):f_it->second;
@@ -90,6 +92,7 @@ exprt verify_encodingt::operator()(const exprt &expr) const
     exprt instance=instantiate(result, e);
 
     return instance;
+    return expr;
   }
   else
   {