From 14a76a0ed54b7c91b7d5bb0b22006974bc82e3bd Mon Sep 17 00:00:00 2001
From: Qinheping Hu <qinhh@amazon.com>
Date: Fri, 13 Sep 2024 14:51:42 -0500
Subject: [PATCH] Clarify usage of history variables in error messages

---
 src/solvers/smt2/smt2_conv.cpp | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 0269cf67e69..8a480746887 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -2476,6 +2476,18 @@ void smt2_convt::convert_expr(const exprt &expr)
       out << ')';
     }
   }
+  else if(expr.id() == ID_old)
+  {
+    UNEXPECTEDCASE(
+      "Invalid usage of old expressions detected. old expressions must be "
+      "used in function contracts.");
+  }
+  else if(expr.id() == ID_loop_entry)
+  {
+    UNEXPECTEDCASE(
+      "Invalid usage of loop_entry expressions detected. loop_entry "
+      "expressions must be used in function contracts.");
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,