diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java index 0f747660..54b6bff7 100644 --- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java +++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VCFolding.java @@ -94,6 +94,12 @@ private Expression foldUnary(UnaryExpression unary) { */ private Expression foldIte(Ite ite) { Expression condition = ite.getCondition(); + + // true ? x : y -> x + // false ? x : y -> y + if (condition instanceof LiteralBoolean literal) + return literal.isBooleanTrue() ? ite.getThen().clone() : ite.getElse().clone(); + Expression foldedCondition = fold(condition); if (!condition.equals(foldedCondition)) return new Ite(foldedCondition, ite.getThen().clone(), ite.getElse().clone()); @@ -108,11 +114,6 @@ private Expression foldIte(Ite ite) { if (!elseExpression.equals(foldedElse)) return new Ite(condition.clone(), thenExpression.clone(), foldedElse); - // true ? x : y -> x - // false ? x : y -> y - if (condition instanceof LiteralBoolean literal) - return literal.isBooleanTrue() ? thenExpression : elseExpression; - // y ? x : x -> x if (thenExpression.equals(elseExpression)) return thenExpression;