Skip to content

Commit fba46eb

Browse files
committed
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.
1 parent 3e66d13 commit fba46eb

File tree

1 file changed

+1
-5
lines changed

1 file changed

+1
-5
lines changed

src/smvlang/smv_typecheck.cpp

Lines changed: 1 addition & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -1720,11 +1720,7 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)
17201720
{
17211721
const std::string &identifier=expr.get_string(ID_identifier);
17221722

1723-
if(identifier=="TRUE")
1724-
expr=true_exprt();
1725-
else if(identifier=="FALSE")
1726-
expr=false_exprt();
1727-
else if(identifier.find("::")==std::string::npos)
1723+
if(identifier.find("::") == std::string::npos)
17281724
{
17291725
std::string id=module+"::var::"+identifier;
17301726

0 commit comments

Comments
 (0)