Merge pull request #5682 from tautschnig/no-propagation

goto_symext::apply_goto_condition must honour --no-propagation

Author: tautschnig

regression/cbmc/no-propagation/main.c

@@ -0,0 +1,6 @@
+int main()
+{
+  int x;
+  if(x == 1)
+    __CPROVER_assert(x == 1, "");
+}

regression/cbmc/no-propagation/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+--no-propagation
+Generated 1 VCC\(s\), 1 remaining after simplification
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

src/goto-symex/symex_goto.cpp

@@ -53,6 +53,9 @@ void goto_symext::apply_goto_condition(
     &jump_not_taken_state.value_set,
     ns);
 
+  if(!symex_config.constant_propagation)
+    return;
+
   jump_taken_state.apply_condition(new_guard, current_state, ns);
 
   // Could use not_exprt + simplify, but let's avoid paying that cost on quite