From fba46eb15836e43e9b80d2ed4352fe2f4e4b01e7 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 10 Jul 2025 17:06:36 -0700 Subject: [PATCH] SMV: TRUE/FALSE are keywords The SMV scanner generates separate tokens for the TRUE/FALSE keywords; hence, there is no need to recognise these as special identifiers in the type checker. --- src/smvlang/smv_typecheck.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/smvlang/smv_typecheck.cpp b/src/smvlang/smv_typecheck.cpp index f5bc8ea2e..b3f584248 100644 --- a/src/smvlang/smv_typecheck.cpp +++ b/src/smvlang/smv_typecheck.cpp @@ -1720,11 +1720,7 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode) { const std::string &identifier=expr.get_string(ID_identifier); - if(identifier=="TRUE") - expr=true_exprt(); - else if(identifier=="FALSE") - expr=false_exprt(); - else if(identifier.find("::")==std::string::npos) + if(identifier.find("::") == std::string::npos) { std::string id=module+"::var::"+identifier;