Promote set_all_frozen to decision_proceduret to remove a dynamic_cast

src/goto-checker/single_loop_incremental_symex_checker.cpp

@@ -42,11 +42,9 @@ single_loop_incremental_symex_checkert::single_loop_incremental_symex_checkert(
 {
   setup_symex(symex, ns, options, ui_message_handler);
 
-  // Freeze all symbols if we are using a prop_conv_solvert
-  prop_conv_solvert *prop_conv_solver = dynamic_cast<prop_conv_solvert *>(
-    &property_decider.get_decision_procedure());
-  if(prop_conv_solver != nullptr)
-    prop_conv_solver->set_all_frozen();
+  // Freeze all symbols (will be a no-op unless we are using a
+  // prop_conv_solvert)
+  property_decider.get_decision_procedure().set_all_frozen();
 }
 
 void output_incremental_status(

src/solvers/decision_procedure.h

@@ -40,6 +40,12 @@ class decision_proceduret
   /// but solver-specific representation.
   virtual exprt handle(const exprt &) = 0;
 
+  /// Make sure simplification steps internal to the decision procedure do not
+  /// result in variables being removed.
+  virtual void set_all_frozen()
+  {
+  }
+
   /// Result of running the decision procedure
   enum class resultt
   {

src/solvers/prop/prop_conv_solver.h

@@ -54,7 +54,7 @@ class prop_conv_solvert : public conflict_providert,
 
   void set_frozen(literalt);
   void set_frozen(const bvt &);
-  void set_all_frozen();
+  void set_all_frozen() override;
 
   literalt convert(const exprt &expr) override;
   bool is_in_conflict(const exprt &expr) const override;