Do not construct a namespace ad hoc when the environment provides one

tautschnig · tautschnig · commit 469895b2d674 · 2022-11-19T23:00:57.000Z
The empty namespace will lack symbol information that may be needed, and
is just unnecessary anyway.
diff --git a/src/goto-instrument/cover_instrument_assume.cpp b/src/goto-instrument/cover_instrument_assume.cpp
@@ -23,8 +23,7 @@ void cover_assume_instrumentert::instrument(
 {
   if(i_it->is_assume())
   {
-    const auto assume_condition =
-      expr2c(i_it->condition(), namespacet{symbol_tablet()});
+    const auto assume_condition = expr2c(i_it->condition(), ns);
     const auto comment_before =
       "assert(false) before assume(" + assume_condition + ")";
     const auto comment_after =

Original file line number	Diff line number	Diff line change
`@@ -23,8 +23,7 @@ void cover_assume_instrumentert::instrument(`
`23`	`23`	`{`
`24`	`24`	`if(i_it->is_assume())`
`25`	`25`	`{`
`26`		`- const auto assume_condition =`
`27`		`- expr2c(i_it->condition(), namespacet{symbol_tablet()});`
	`26`	`+ const auto assume_condition = expr2c(i_it->condition(), ns);`
`28`	`27`	`const auto comment_before =`
`29`	`28`	`"assert(false) before assume(" + assume_condition + ")";`
`30`	`29`	`const auto comment_after =`