From bb2bf86c88e37849800e8aec0b17c259ce725636 Mon Sep 17 00:00:00 2001
From: Andrii <andrii@asymptotic.tech>
Date: Tue, 12 May 2026 16:55:50 +0300
Subject: [PATCH] big boogie chash trace inconclusive type
 (check_is_fix_coin_a_spec)

---
 .../SMTLib/SMTLibBatchTheoremProver.cs        |  1 +
 .../SMTLib/SMTLibInteractiveTheoremProver.cs  | 10 +++---
 .../SMTLib/SMTLibProcessTheoremProver.cs      | 34 +++++++++++++++++++
 3 files changed, 41 insertions(+), 4 deletions(-)

diff --git a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
index 6b2221c62..72996f75d 100644
--- a/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibBatchTheoremProver.cs
@@ -116,6 +116,7 @@ public override void FullReset(VCExpressionGenerator generator)
       this.gen = generator;
       SendThisVC("(reset)");
       common.Clear();
+      ClearPushSnapshots();
       SetupAxiomBuilder(gen);
       namer = GetNamer(libOptions, options);
       Axioms.Clear();
diff --git a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
index c20327d01..a57ae1c29 100644
--- a/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibInteractiveTheoremProver.cs
@@ -98,8 +98,7 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
           finalNamer = ResetNamer(commonNamer);
         }
 
-        SendThisVC("(push 1)");
-        DeclCollector.Push();
+        Push();
         string vcString = "(assert (not\n" + VCExpr2String(vc, 1) + "\n))";
         FlushAxioms();
         SendVCId(descriptiveName);
@@ -116,15 +115,17 @@ public override async Task<SolverOutcome> Check(string descriptiveName, VCExpr v
           Process.NewProblem(descriptiveName);
         }
 
-        DeclCollector.Pop();
         if (hasReset)
         {
           common = new StringBuilder(CachedCommon);
           hasReset = false;
+          // The push snapshot captured the pre-reset `common.Length`; re-anchor
+          // it so Pop() truncates relative to the swapped-in buffer.
+          ReanchorTopPushSnapshot();
         }
 
         var result = await CheckSat(cancellationToken, errorLimit);
-        SendThisVC("(pop 1)");
+        Pop();
 
         return result;
       }
@@ -172,6 +173,7 @@ public override void FullReset(VCExpressionGenerator generator)
       finalNamer = null;
       hasReset = true;
       common.Clear();
+      ClearPushSnapshots();
       SetupAxiomBuilder(gen);
       Axioms.Clear();
       TypeDecls.Clear();
diff --git a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
index e88022c23..4cdedb98b 100644
--- a/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
+++ b/Source/Provers/SMTLib/SMTLibProcessTheoremProver.cs
@@ -29,6 +29,12 @@ public abstract class SMTLibProcessTheoremProver : ProverInterface
     protected bool HadErrors { get; set; }
     
     protected StringBuilder common = new();
+    // Snapshots of `common.Length` taken at each Push(). Pop() truncates
+    // `common` back, so per-VC declarations sent via SendCommon inside a
+    // push frame do not survive past it. Otherwise PossiblyRestart would
+    // replay them to a fresh solver and DeclCollector would redeclare them
+    // on the next Check, producing "already declared" errors.
+    private readonly Stack<int> commonLengthsBeforePush = new();
     protected string CachedCommon = null;
     protected TextWriter currentLogFile;
     protected volatile ErrorHandler currentErrorHandler;
@@ -1113,6 +1119,33 @@ public override void Pop()
     {
       SendThisVC("(pop 1)");
       DeclCollector.Pop();
+      if (commonLengthsBeforePush.Count > 0)
+      {
+        var snapshot = commonLengthsBeforePush.Pop();
+        if (common.Length > snapshot)
+        {
+          common.Length = snapshot;
+        }
+      }
+    }
+
+    /// Replace the top push-snapshot with the current `common.Length`. Used
+    /// when `common` is swapped out between a Push() and matching Pop() (for
+    /// example after `(reset)` / cached-common restore).
+    protected void ReanchorTopPushSnapshot()
+    {
+      if (commonLengthsBeforePush.Count > 0)
+      {
+        commonLengthsBeforePush.Pop();
+        commonLengthsBeforePush.Push(common.Length);
+      }
+    }
+
+    /// Discard all outstanding push-snapshots. Used by FullReset implementations
+    /// that wipe `common` so stale offsets don't try to truncate the fresh buffer.
+    protected void ClearPushSnapshots()
+    {
+      commonLengthsBeforePush.Clear();
     }
 
     public override int NumAxiomsPushed()
@@ -1545,6 +1578,7 @@ protected int ParseRCount(SExpr resp)
 
     public override void Push()
     {
+      commonLengthsBeforePush.Push(common.Length);
       SendThisVC("(push 1)");
       DeclCollector.Push();
     }