From 83f5c48badcd0f02dc652f6a64690c0772a95201 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Wed, 18 Sep 2024 00:18:32 -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..4c9ccc12b0e 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 loop invariants."); + } else INVARIANT_WITH_DIAGNOSTICS( false,