From 694202b950157a38c9455b372bed0b2bad2d2797 Mon Sep 17 00:00:00 2001
From: Ricardo Costa <rcosta.ms358@gmail.com>
Date: Mon, 6 Apr 2026 15:15:14 +0100
Subject: [PATCH] Make Counterexample Filtering Order Insensitive

---
 .../liquidjava/diagnostics/errors/RefinementError.java | 10 ++++++----
 .../java/liquidjava/rj_language/ast/Expression.java    | 10 ++++++++++
 2 files changed, 16 insertions(+), 4 deletions(-)

diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
index 39a81d92..149e5496 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
@@ -5,6 +5,7 @@
 import java.util.stream.Collectors;
 
 import liquidjava.diagnostics.TranslationTable;
+import liquidjava.rj_language.ast.Expression;
 import liquidjava.rj_language.opt.derivation_node.ValDerivationNode;
 import liquidjava.smt.Counterexample;
 import liquidjava.utils.VariableFormatter;
@@ -46,16 +47,17 @@ public String getCounterExampleString() {
 
         List<String> foundVarNames = new ArrayList<>();
         found.getValue().getVariableNames(foundVarNames);
+        List<String> foundAssignments = found.getValue().getConjuncts().stream().map(Expression::toString).toList();
         String counterexampleString = counterexample.assignments().stream()
-                // only include variables that appear in the found value
-                .filter(a -> foundVarNames.contains(a.first()))
+                // only include variables that appear in the found value and are not already fixed there
+                .filter(a -> foundVarNames.contains(a.first())
+                        && !foundAssignments.contains(a.first() + " == " + a.second()))
                 // format as "var == value"
                 .map(a -> VariableFormatter.formatVariable(a.first()) + " == " + a.second())
                 // join with "&&"
                 .collect(Collectors.joining(" && "));
 
-        String foundString = VariableFormatter.formatText(found.getValue().toString());
-        if (counterexampleString.isEmpty() || counterexampleString.equals(foundString))
+        if (counterexampleString.isEmpty())
             return null;
 
         return counterexampleString;
diff --git a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
index 3859c530..1f1a91dc 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/rj_language/ast/Expression.java
@@ -81,6 +81,16 @@ public boolean isBooleanExpression() {
         return false;
     }
 
+    public List<Expression> getConjuncts() {
+        if (this instanceof BinaryExpression binaryExpression && "&&".equals(binaryExpression.getOperator())) {
+            List<Expression> conjuncts = new ArrayList<>();
+            conjuncts.addAll(binaryExpression.getFirstOperand().getConjuncts());
+            conjuncts.addAll(binaryExpression.getSecondOperand().getConjuncts());
+            return conjuncts;
+        }
+        return List.of(this);
+    }
+
     /**
      * Substitutes the expression first given expression by the second
      *