Clarify usage of history variables in error messages

qinheping · Sep 13, 2024 · 6353af4 · 6353af4
1 parent 2212cd6
commit 6353af4
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 __CPROVER_old detected. __CPROVER_old must be used in "
+      "function contracts.");
+  }
+  else if(expr.id() == ID_loop_entry)
+  {
+    UNEXPECTEDCASE(
+      "Invalid usage of __CPROVER_loop_entry detected. __CPROVER_loop_entry "
+      "must be used in function contracts.");
+  }
   else
     INVARIANT_WITH_DIAGNOSTICS(
       false,