Handle unconditional loop during synthesis

Author: qinheping

src/goto-synthesizer/enumerative_loop_contracts_synthesizer.cpp

@@ -100,13 +100,13 @@ void enumerative_loop_contracts_synthesizert::init_candidates()
       // we only synthesize invariants and assigns for unannotated loops
       if(loop_end->condition().find(ID_C_spec_loop_invariant).is_nil())
       {
-        // Store the loop guard.
-        exprt guard =
-          get_loop_head(
-            loop_end->loop_number,
-            goto_model.goto_functions.function_map[function_p.first])
-            ->condition();
-        neg_guards[new_id] = guard;
+        // Store the loop guard if exists.
+        auto loop_head = get_loop_head(
+          loop_end->loop_number,
+          goto_model.goto_functions.function_map[function_p.first]);
+
+        if(loop_head->has_condition())
+          neg_guards[new_id] = loop_head->condition();
 
         // Initialize invariant clauses as `true`.
         in_invariant_clause_map[new_id] = true_exprt();

src/goto-synthesizer/synthesizer_utils.cpp

@@ -144,18 +144,26 @@ invariant_mapt combine_in_and_post_invariant_clauses(
   const invariant_mapt &neg_guards)
 {
   // Combine invariant
-  // (in_inv || !guard) && (!guard -> pos_inv)
+  // (in_inv || !guard) && (!guard -> pos_inv) for loops with loop guard
+  // in_inv && pos_inv for loops without loop guard
   invariant_mapt result;
   for(const auto &in_clause : in_clauses)
   {
     const auto &id = in_clause.first;
     const auto &it_guard = neg_guards.find(id);
 
-    INVARIANT(it_guard != neg_guards.end(), "Some loop guard is missing.");
-
-    result[id] = and_exprt(
-      or_exprt(it_guard->second, in_clause.second),
-      implies_exprt(it_guard->second, post_clauses.at(id)));
+    // Unconditional loop or failed to get loop guard.
+    if(it_guard == neg_guards.end())
+    {
+      result[id] = and_exprt(in_clause.second, post_clauses.at(id));
+    }
+    // Loops with loop guard.
+    else
+    {
+      result[id] = and_exprt(
+        or_exprt(it_guard->second, in_clause.second),
+        implies_exprt(it_guard->second, post_clauses.at(id)));
+    }
   }
   return result;
 }