use satisfying_assignment() method

Daniel Kroening · Daniel Kroening · commit bcd05d835221 · 2016-08-19T10:53:17.000+01:00
diff --git a/src/cbmc/bmc_cover.cpp b/src/cbmc/bmc_cover.cpp
@@ -88,7 +88,8 @@ class bmc_covert:
   
   bool operator()();
 
-  virtual void goal_covered(const cover_goalst::goalt &);
+  // gets called by prop_covert
+  virtual void satisfying_assignment();
 
   struct goalt
   {
@@ -183,7 +184,7 @@ class bmc_covert:
 
 /*******************************************************************\
 
-Function: bmc_covert::goal_covered
+Function: bmc_covert::satisfying_assignment
 
   Inputs:
 
@@ -193,7 +194,7 @@ Function: bmc_covert::goal_covered
 
 \*******************************************************************/
 
-void bmc_covert::goal_covered(const cover_goalst::goalt &)
+void bmc_covert::satisfying_assignment()
 {
   for(auto &g_it : goal_map)
   {

Original file line number	Diff line number	Diff line change
`@@ -88,7 +88,8 @@ class bmc_covert:`
`88`	`88`
`89`	`89`	`bool operator()();`
`90`	`90`
`91`		`- virtual void goal_covered(const cover_goalst::goalt &);`
	`91`	`+ // gets called by prop_covert`
	`92`	`+ virtual void satisfying_assignment();`
`92`	`93`
`93`	`94`	`struct goalt`
`94`	`95`	`{`
`@@ -183,7 +184,7 @@ class bmc_covert:`
`183`	`184`
`184`	`185`	`/*******************************************************************\`
`185`	`186`
`186`		`-Function: bmc_covert::goal_covered`
	`187`	`+Function: bmc_covert::satisfying_assignment`
`187`	`188`
`188`	`189`	`Inputs:`
`189`	`190`
`@@ -193,7 +194,7 @@ Function: bmc_covert::goal_covered`
`193`	`194`
`194`	`195`	`\*******************************************************************/`
`195`	`196`
`196`		`-void bmc_covert::goal_covered(const cover_goalst::goalt &)`
	`197`	`+void bmc_covert::satisfying_assignment()`
`197`	`198`	`{`
`198`	`199`	`for(auto &g_it : goal_map)`
`199`	`200`	`{`