Symex: always generate an assumption when truncating a path

Whenever we truncate a particular execution path, whether due to --unwind or --depth settings,
we should generate an assumption so that it is not necessary to record the rejected path in the
state guard.

For example, before if we exceeded the depth limit then we would set the guard to false, and rely
on carrying this missing path forwards to any future assume or assert statement. By emitting an
assume we explicitly make a constraint ruling this path out, meaning that downstream guards no
longer need to carry that information (for example, where before we might have had guard `x` and
VCCs `!x => y` and `!x => z`, we can now emit a constraint `!x`, restore the guard to `true` and
produce VCCs `y` and `z`).

Note this commit does not actually change when the guard is set false and when it is not, as this
will have additional performance consequences and should be benchmarked independently.

Author: smowton

src/goto-symex/symex_function_call.cpp

@@ -258,7 +258,10 @@ void goto_symext::symex_function_call_code(
       if(symex_config.unwinding_assertions)
         vcc(false_exprt(), "recursion unwinding assertion", state);
 
-      // add to state guard to prevent further assignments
+      // Rule out this path:
+      symex_assume_l2(state, false_exprt());
+      // Disable processing instructions until we next encounter one reachable
+      // without passing this instruction:
       state.guard.add(false_exprt());
     }
 

src/goto-symex/symex_goto.cpp

@@ -795,15 +795,16 @@ void goto_symext::loop_bound_exceeded(
         negated_cond,
         "unwinding assertion loop " + std::to_string(loop_number),
         state);
+    }
+
+    // generate unwinding assumption, unless we permit partial loops
+    symex_assume_l2(state, negated_cond);
 
+    if(symex_config.unwinding_assertions)
+    {
       // add to state guard to prevent further assignments
       state.guard.add(negated_cond);
     }
-    else
-    {
-      // generate unwinding assumption, unless we permit partial loops
-      symex_assume_l2(state, negated_cond);
-    }
   }
 }
 

src/goto-symex/symex_main.cpp

@@ -528,7 +528,13 @@ void goto_symext::execute_next_instruction(
 
   // depth exceeded?
   if(symex_config.max_depth != 0 && state.depth > symex_config.max_depth)
+  {
+    // Rule out this path:
+    symex_assume_l2(state, false_exprt());
+    // Disable processing instructions until we next encounter one reachable
+    // without passing this instruction:
     state.guard.add(false_exprt());
+  }
   state.depth++;
 
   // actually do instruction