diff --git a/include/runtime/proof_trace_writer.h b/include/runtime/proof_trace_writer.h index 810d54cdd..2e199c247 100644 --- a/include/runtime/proof_trace_writer.h +++ b/include/runtime/proof_trace_writer.h @@ -285,6 +285,8 @@ class proof_trace_callback_writer : public proof_trace_writer { std::optional 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()); + } } }