Merge pull request #1193 from diffblue/smvlang-TRUE-FALSE

tautschnig · web-flow · commit 8b76c4ece296 · 2025-07-11T14:06:36.000+02:00
SMV: `TRUE`/`FALSE` are keywords
diff --git 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;
 

Original file line number	Diff line number	Diff line change
`@@ -1720,11 +1720,7 @@ void smv_typecheckt::convert(exprt &expr, expr_modet expr_mode)`
`1720`	`1720`	`{`
`1721`	`1721`	`const std::string &identifier=expr.get_string(ID_identifier);`
`1722`	`1722`
`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)`
`1728`	`1724`	`{`
`1729`	`1725`	`std::string id=module+"::var::"+identifier;`
`1730`	`1726`