Improve error for assumption scope

cvc5 · Dec 20, 2024 · 4331a9d · 4331a9d
1 parent 216d384
commit 4331a9d
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/state.cpp b/src/state.cpp
@@ -321,8 +321,9 @@ bool State::includeFile(const std::string& s, bool isSignature, bool isReference
   Trace("state") << "...finished" << std::endl;
   if (getAssumptionLevel()!=0)
   {
+    Assert(!d_declsSizeCtx.empty() && d_declsSizeCtx.back()<d_decls.size());
     EO_FATAL() << "Including file " << inputPath.getRawPath()
-                 << " did not preserve assumption scope";
+                 << " did not preserve assumption scope. The most recent open assumption was " << d_decls[d_declsSizeCtx.back()] << ".";
   }
   return true;
 }