Clarify usage of history variables in error messages

diffblue · Sep 13, 2024 · d5b6966 · d5b6966
1 parent 2212cd6
commit d5b6966
Showing 1 changed file with 12 additions and 0 deletions.
diff --git 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,