Has_properties check must be in incremental_goto_checker

peterschrammel · peterschrammel · commit 39d25d71d9ac · 2019-04-16T11:57:37.000+01:00
With symex-driven-lazy-loading there might not be any
properties initially.
diff --git a/src/goto-checker/all_properties_verifier.h b/src/goto-checker/all_properties_verifier.h
@@ -35,10 +35,6 @@ class all_properties_verifiert : public goto_verifiert
 
   resultt operator()() override
   {
-    // have we got anything to check? otherwise we return PASS
-    if(!has_properties_to_check(properties))
-      return resultt::PASS;
-
     while(incremental_goto_checker(properties).progress !=
           incremental_goto_checkert::resultt::progresst::DONE)
     {

Original file line number	Diff line number	Diff line change
`@@ -35,10 +35,6 @@ class all_properties_verifiert : public goto_verifiert`
`35`	`35`
`36`	`36`	`resultt operator()() override`
`37`	`37`	`{`
`38`		`- // have we got anything to check? otherwise we return PASS`
`39`		`- if(!has_properties_to_check(properties))`
`40`		`- return resultt::PASS;`
`41`		`-`
`42`	`38`	`while(incremental_goto_checker(properties).progress !=`
`43`	`39`	`incremental_goto_checkert::resultt::progresst::DONE)`
`44`	`40`	`{`