From e67da6595bc3d7d593d2de5891bffb416e8c52ea Mon Sep 17 00:00:00 2001
From: Daniel Balasubramanian <danielbala@gmail.com>
Date: Thu, 30 May 2024 13:40:05 -0500
Subject: [PATCH] Assert equality between user constants that unify to the same
 variable in a match

---
 Src/Core/Common/Rules/CoreRule.cs | 26 ++++++++++++++++++++++++++
 1 file changed, 26 insertions(+)

diff --git a/Src/Core/Common/Rules/CoreRule.cs b/Src/Core/Common/Rules/CoreRule.cs
index dc03b4d..841870e 100644
--- a/Src/Core/Common/Rules/CoreRule.cs
+++ b/Src/Core/Common/Rules/CoreRule.cs
@@ -1452,6 +1452,32 @@ private bool ApplyMatch(SymExecuter facts, Matcher m, Term t, int bindingLevel)
                 return false;
             }
 
+            foreach (var item in partitions)
+            {
+                var curr = item.Value;
+                List<Term> terms = new List<Term>();
+                if (curr.Count > 2)
+                {
+                    foreach (var term in curr)
+                    {
+                        if (term.Symbol is UserCnstSymb && term.Groundness == Groundness.Variable)
+                        {
+                            UserCnstSymb userCnstSymb = (UserCnstSymb)term.Symbol;
+                            if (userCnstSymb.IsAutoGen && userCnstSymb.Name.StartsWith("pm@"))
+                            {
+                                terms.Add(term);
+                            }
+                        }
+                    }
+
+                    for (int i = 0; i < terms.Count - 1; i++)
+                    {
+                        facts.PendEqualityConstraint(terms[i], terms[i + 1]);
+                    }
+                }
+
+            }
+
             return true;
         }