Callbacks: Fix side-condition events when arity is non-null (#1194)

This PR fixes a bug in calls to calls to
`side_condition_event_callback`. Every time such a call should occur,
the `rewrite_event_callback` is invoked instead.

This is due to a bug in the method that builds substitutions, and calls
a callback once the substitution has the required size. Instead of
conditionally calling either the rewrite callback or the sidecondition
callback, it always calls the rewrite one.

This PR fixes the bug.

---------

Co-authored-by: Theodoros Kasampalis <[email protected]>

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());
+      }
     }
   }