Update SMTEncoder.cpp

soniseth0 · web-flow · commit c47308bf68ed · 2025-11-28T23:23:57.000+01:00
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
@@ -1297,7 +1297,7 @@ void SMTEncoder::endVisit(Literal const& _literal)
 	if (smt::isNumber(type))
 		defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));
 	else if (smt::isBool(type))
-		defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));
+		defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral));
 	else if (smt::isStringLiteral(type))
 	{
 		createExpr(_literal);

Original file line number	Diff line number	Diff line change
`@@ -1297,7 +1297,7 @@ void SMTEncoder::endVisit(Literal const& _literal)`
`1297`	`1297`	`if (smt::isNumber(type))`
`1298`	`1298`	`defineExpr(_literal, smtutil::Expression(type.literalValue(&_literal)));`
`1299`	`1299`	`else if (smt::isBool(type))`
`1300`		`- defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral ? true : false));`
	`1300`	`+ defineExpr(_literal, smtutil::Expression(_literal.token() == Token::TrueLiteral));`
`1301`	`1301`	`else if (smt::isStringLiteral(type))`
`1302`	`1302`	`{`
`1303`	`1303`	`createExpr(_literal);`