big boogie chash trace inconclusive type (check_is_fix_coin_a_spec)

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

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

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