From 88bf3c6e516276bb813b2e57be6309aec529a9a3 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 31 Jan 2023 13:35:43 -0800
Subject: [PATCH] check if trail is empty to avoid collecting variables

---
 src/ast/simplifiers/model_reconstruction_trail.cpp | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/ast/simplifiers/model_reconstruction_trail.cpp b/src/ast/simplifiers/model_reconstruction_trail.cpp
index 65635c8e4..95f73fd7a 100644
--- a/src/ast/simplifiers/model_reconstruction_trail.cpp
+++ b/src/ast/simplifiers/model_reconstruction_trail.cpp
@@ -25,6 +25,9 @@ Author:
 
 void model_reconstruction_trail::replay(unsigned qhead, expr_ref_vector& assumptions, dependent_expr_state& st) {
 
+    if (m_trail.empty())
+        return;
+
     ast_mark free_vars;
     m_intersects_with_model = false;
     scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m, false);