From 22aba74176639c70e97a98ea86e3272354c02349 Mon Sep 17 00:00:00 2001 From: chriseth Date: Sun, 20 Mar 2022 21:52:26 +0100 Subject: [PATCH] Simplify condition. --- libyul/optimiser/ReasoningBasedSimplifier.cpp | 10 ++++------ 1 file changed, 4 insertions(+), 6 deletions(-) diff --git a/libyul/optimiser/ReasoningBasedSimplifier.cpp b/libyul/optimiser/ReasoningBasedSimplifier.cpp index c14212e16..a420b2020 100644 --- a/libyul/optimiser/ReasoningBasedSimplifier.cpp +++ b/libyul/optimiser/ReasoningBasedSimplifier.cpp @@ -263,17 +263,15 @@ smtutil::Expression ReasoningBasedSimplifier::encodeEVMBuiltin( return booleanValue(arguments.at(0) == constantValue(0)); case evmasm::Instruction::AND: return smtutil::Expression::ite( - (arguments.at(0) == 0 || arguments.at(0) == 1) && - (arguments.at(1) == 0 || arguments.at(1) == 1), - booleanValue(arguments.at(0) == 1 && arguments.at(1) == 1), + arguments.at(0) + arguments.at(1) <= 2, + booleanValue(arguments.at(0) + arguments.at(1) >= 2), // TODO we could probably restrict it a bit more newRestrictedVariable() ); case evmasm::Instruction::OR: return smtutil::Expression::ite( - (arguments.at(0) == 0 || arguments.at(0) == 1) && - (arguments.at(1) == 0 || arguments.at(1) == 1), - booleanValue(arguments.at(0) == 1 || arguments.at(1) == 1), + arguments.at(0) + arguments.at(1) <= 2, + booleanValue(arguments.at(0) + arguments.at(1) >= 1), // TODO we could probably restrict it a bit more newRestrictedVariable() );