Explicitly scolemise quantifier bound variables in goto_check_rec.

Add a special case handling for `forall` and `exists` expressions to
have their bound variables instantiated by a new symbol, in effect
performing a scolem transformation over it.

Author: NlightNFotis

src/analyses/goto_check.cpp

@@ -22,9 +22,11 @@ Author: Daniel Kroening, [email protected]
 #include <util/expr_util.h>
 #include <util/find_symbols.h>
 #include <util/floatbv_expr.h>
+#include <util/fresh_symbol.h>
 #include <util/ieee_float.h>
 #include <util/invariant.h>
 #include <util/make_unique.h>
+#include <util/mathematical_expr.h>
 #include <util/options.h>
 #include <util/pointer_expr.h>
 #include <util/pointer_offset_size.h>
@@ -1747,6 +1749,26 @@ void goto_checkt::check_rec(const exprt &expr, guardt &guard)
     if(check_rec_member(to_member_expr(expr), guard))
       return;
   }
+  else if(expr.id() == ID_forall || expr.id() == ID_exists)
+  {
+    // In the case of a quantified statement, skolemise the expression
+    // and recurse.
+    const auto quantified_expr = to_quantifier_expr(expr);
+    const auto quantifier_sym = quantified_expr.symbol();
+    const auto new_symbol = get_fresh_aux_symbol(
+      quantifier_sym.type(),
+      CPROVER_PREFIX,
+      id2string(ns.lookup(quantifier_sym.get_identifier()).base_name),
+      quantified_expr.source_location(),
+      ID_C,
+      const_cast<symbol_table_baset &>(ns.get_symbol_table()));
+    const auto symbol_expr =
+      symbol_exprt(new_symbol.name, quantifier_sym.type());
+    const std::vector<exprt> new_sym_vec{symbol_expr};
+    const auto instantiated_expr = quantified_expr.instantiate(new_sym_vec);
+    check_rec(instantiated_expr, guard);
+    return;
+  }
 
   forall_operands(it, expr)
     check_rec(*it, guard);