(Not needed?) direct symbol evaluations

owen-mc-diffblue · owen-mc-diffblue · commit 2cca3cd8a827 · 2019-09-08T08:16:54.000+01:00
diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp
@@ -125,6 +125,16 @@ void goto_statet::apply_condition(
       }
     }
   }
+  else if(condition.id() == ID_symbol)
+  {
+    if(condition.type() == bool_typet())
+    {
+      // A
+      // -->
+      // A == true
+      apply_condition(equal_exprt(condition, true_exprt()), previous_state, ns);
+    }
+  }
   else if(
     condition.id() == ID_notequal &&
     skip_typecast(to_notequal_expr(condition).lhs()).type().id() == ID_c_bool)

Original file line number	Diff line number	Diff line change
`@@ -125,6 +125,16 @@ void goto_statet::apply_condition(`
`125`	`125`	`}`
`126`	`126`	`}`
`127`	`127`	`}`
	`128`	`+ else if(condition.id() == ID_symbol)`
	`129`	`+ {`
	`130`	`+ if(condition.type() == bool_typet())`
	`131`	`+ {`
	`132`	`+ // A`
	`133`	`+ // -->`
	`134`	`+ // A == true`
	`135`	`+ apply_condition(equal_exprt(condition, true_exprt()), previous_state, ns);`
	`136`	`+ }`
	`137`	`+ }`
`128`	`138`	`else if(`
`129`	`139`	`condition.id() == ID_notequal &&`
`130`	`140`	`skip_typecast(to_notequal_expr(condition).lhs()).type().id() == ID_c_bool)`