const & protect goto_symext::constant_propagation

This member is never written to and serves merely as a cache for a
front-end option, so this commit makes it const and protected.

Author: karkhaz

src/cbmc/bmc.h

@@ -86,7 +86,6 @@ class bmct:public safety_checkert
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
-    symex.constant_propagation=options.get_bool_option("propagation");
     symex.record_coverage=
       !options.get_option("symex-coverage-report").empty();
     symex.self_loops_to_assumptions =
@@ -162,7 +161,6 @@ class bmct:public safety_checkert
       ui_message_handler(_message_handler),
       driver_callback_after_symex(callback_after_symex)
   {
-    symex.constant_propagation = options.get_bool_option("propagation");
     symex.record_coverage =
       !options.get_option("symex-coverage-report").empty();
     INVARIANT(

src/goto-instrument/accelerate/scratch_program.cpp

@@ -35,7 +35,6 @@ bool scratch_programt::check_sat(bool do_slice)
   output(ns, "scratch", std::cout);
 #endif
 
-  symex.constant_propagation=constant_propagation;
   goto_symex_statet::propagationt::valuest constants;
 
   symex.symex_with_state(symex_state, functions, symex_symbol_table);

src/goto-symex/goto_symex.h

@@ -62,9 +62,9 @@ class goto_symext
         options.get_bool_option("allow-pointer-unsoundness")),
       total_vccs(0),
       remaining_vccs(0),
-      constant_propagation(true),
       self_loops_to_assumptions(true),
       language_mode(),
+      constant_propagation(options.get_bool_option("propagation")),
       outer_symbol_table(outer_symbol_table),
       ns(outer_symbol_table),
       target(_target),
@@ -212,14 +212,15 @@ class goto_symext
   // statistics
   unsigned total_vccs, remaining_vccs;
 
-  bool constant_propagation;
   bool self_loops_to_assumptions;
 
   /// language_mode: ID_java, ID_C or another language identifier
   /// if we know the source language in use, irep_idt() otherwise.
   irep_idt language_mode;
 
 protected:
+  const bool constant_propagation;
+
   /// The symbol table associated with the goto-program that we're
   /// executing. This symbol table will not additionally contain objects
   /// that are dynamically created as part of symbolic execution; the