Clarify usage of history variables in error messages

qinheping · Sep 18, 2024 · 83f5c48 · 83f5c48
1 parent 2212cd6
commit 83f5c48
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 loop invariants.");
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,