add tests and a valderivation node for this

Author: CatarinaGamboa

liquidjava-verifier/src/main/java/liquidjava/rj_language/opt/VariablePropagation.java

@@ -149,6 +149,18 @@ private static void extractVarOrigins(ValDerivationNode node, Map<String, Deriva
             }
         }
 
+        // Mirror the resolver's bare-internal-var rule (`#x` ⇒ true, `!#x` ⇒ false): point #x's
+        // back-link at the conjunct that justified the substitution, so subsequent passes preserve
+        // provenance through these substitutions too.
+        if (value instanceof Var var && var.getName().startsWith("#")) {
+            DerivationNode back = origin != null ? origin : node;
+            varOrigins.putIfAbsent(var.getName(), back);
+        } else if (value instanceof UnaryExpression u && "!".equals(u.getOp()) && u.getExpression()instanceof Var inner
+                && inner.getName().startsWith("#")) {
+            DerivationNode back = origin != null ? origin : node;
+            varOrigins.putIfAbsent(inner.getName(), back);
+        }
+
         // recursively process the origin tree
         if (origin instanceof BinaryDerivationNode binOrigin) {
             extractVarOrigins(binOrigin.getLeft(), varOrigins);

liquidjava-verifier/src/test/java/liquidjava/rj_language/opt/VariableResolverTest.java

@@ -214,4 +214,33 @@ void testUnusedFunctionInvocationEqualityIsIgnored() {
 
         assertTrue(result.isEmpty(), "Function invocation definitions with no usage should be ignored");
     }
+
+    @Test
+    void testBareNegatedInternalVarSubstitutesFalse() {
+        Expression expression = parse("!#fresh_1 && #fresh_1 == #hasNext_2");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Should extract only the bare-conjunct substitution");
+        assertEquals("false", result.get("#fresh_1").toString(),
+                "!#fresh_1 as top-level conjunct should bind #fresh_1 to false");
+    }
+
+    @Test
+    void testBareInternalVarSubstitutesTrue() {
+        Expression expression = parse("#fresh_1 && #fresh_1 == #hasNext_2");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertEquals(1, result.size(), "Should extract only the bare-conjunct substitution");
+        assertEquals("true", result.get("#fresh_1").toString(),
+                "Bare #fresh_1 as top-level conjunct should bind #fresh_1 to true");
+    }
+
+    @Test
+    void testBareUserVarNotSubstituted() {
+        Expression expression = parse("x && y == x");
+        Map<String, Expression> result = VariableResolver.resolve(expression);
+
+        assertTrue(result.isEmpty(),
+                "Bare user-facing variables should not be substituted, to preserve their names in error messages");
+    }
 }