Merge remote-tracking branch 'origin/develop'

Author: rv-auditor

include/runtime/proof_trace_writer.h

@@ -285,6 +285,8 @@ class proof_trace_callback_writer : public proof_trace_writer {
   std::optional<rewrite_event_construction> current_rewrite_event_{
       std::nullopt};
 
+  bool rewrite_callback_pending_;
+
   virtual void proof_trace_header_callback(uint32_t version) { }
   virtual void hook_event_callback(call_event_construction const &event) { }
   virtual void rewrite_event_callback(rewrite_event_construction const &event) {
@@ -332,6 +334,8 @@ class proof_trace_callback_writer : public proof_trace_writer {
     current_rewrite_event_.emplace(ordinal, arity);
     if (arity == 0) {
       rewrite_event_callback(current_rewrite_event_.value());
+    } else {
+      rewrite_callback_pending_ = true;
     }
   }
 
@@ -345,7 +349,12 @@ class proof_trace_callback_writer : public proof_trace_writer {
     p.second.bits = bits;
     size_t new_pos = ++current_rewrite_event_->pos;
     if (new_pos == current_rewrite_event_->arity) {
-      rewrite_event_callback(current_rewrite_event_.value());
+      if (rewrite_callback_pending_) {
+        rewrite_event_callback(current_rewrite_event_.value());
+        rewrite_callback_pending_ = false;
+      } else {
+        side_condition_event_callback(current_rewrite_event_.value());
+      }
     }
   }