Return updated properties in incremental goto checker result

The goto verifier might want to know which
properties have been updated in the last call to
the incremental goto checker, e.g. to output status information
or report results continuously.

Author: peterschrammel

src/goto-checker/all_properties_verifier.h

@@ -39,8 +39,9 @@ class all_properties_verifiert : public goto_verifiert
     if(!has_properties_to_check(properties))
       return resultt::PASS;
 
-    while(incremental_goto_checker(properties) !=
-          incremental_goto_checkert::resultt::DONE)
+    while(
+      incremental_goto_checker(properties).progress
+        != incremental_goto_checkert::resultt::progresst::DONE)
     {
       // loop until we are done
     }

src/goto-checker/incremental_goto_checker.cpp

@@ -19,3 +19,14 @@ incremental_goto_checkert::incremental_goto_checkert(
     log(ui_message_handler)
 {
 }
+
+incremental_goto_checkert::resultt::resultt()
+  : progress(progresst::DONE)
+{
+}
+
+incremental_goto_checkert::resultt::resultt(
+  progresst progress, const std::vector<irep_idt> &updated_properties)
+  : progress(progress), updated_properties(updated_properties)
+{
+}

src/goto-checker/incremental_goto_checker.h

@@ -37,22 +37,36 @@ class incremental_goto_checkert
   incremental_goto_checkert(const incremental_goto_checkert &) = delete;
   virtual ~incremental_goto_checkert() = default;
 
-  enum class resultt
+  struct resultt
   {
-    /// The goto checker may be able to find another FAILed property
-    /// if operator() is called again.
-    FOUND_FAIL,
-    /// The goto checker has returned all results for the given set
-    /// of properties.
-    DONE
+    enum class progresst
+    {
+      /// The goto checker may be able to find another FAILed property
+      /// if operator() is called again.
+        FOUND_FAIL,
+      /// The goto checker has returned all results for the given set
+      /// of properties.
+        DONE
+    };
+
+    progresst progress;
+
+    /// Changed properties since the last call to
+    /// `incremental_goto_checkert::operator()`
+    std::vector<irep_idt> updated_properties;
+
+    resultt();
+    resultt(
+      progresst progress, const std::vector<irep_idt> &updated_properties);
   };
 
   /// Check whether the given properties with status NOT_CHECKED, UNKNOWN or
   /// properties newly discovered by `goto_checkert` hold.
   /// \param [out] properties: Properties updated to whether their status
   ///   have been determined. Newly discovered properties are added.
   /// \return whether the goto checker found a violated property (FOUND_FAIL) or
-  ///   whether it is DONE with the given properties.
+  ///   whether it is DONE with the given properties, together with
+  ///   the properties whose status changed since the last call to operator().
   /// After returning DONE, another call to operator() with the same
   /// properties will return DONE and leave the properties' status unchanged.
   /// If there is a property with status FAIL then its counterexample