From 3e7cd24814c0f5eb53846f8ef0b167640c7b93d3 Mon Sep 17 00:00:00 2001
From: Markus Triska <triska@metalevel.at>
Date: Mon, 21 Jun 2021 21:19:37 +0200
Subject: [PATCH] address #995: wrong results for popcount/1

Many thanks to @notoria and @flexoron for very useful test cases!
---
 src/lib/clpz.pl | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/lib/clpz.pl b/src/lib/clpz.pl
index 32622f72..f330b36f 100644
--- a/src/lib/clpz.pl
+++ b/src/lib/clpz.pl
@@ -2959,6 +2959,12 @@ expr_conds(popcount(A0), Count) -->
         expr_conds(A0, A),
         [I is A, arithmetic:popcount(I, Count)].
 
+no_popcount_t(Gs, T) :-
+        (   member(arithmetic:popcount(_, _), Gs) ->
+            T = false
+        ;   T = true
+        ).
+
 clpz_expandable(_ in _).
 clpz_expandable(_ #= _).
 clpz_expandable(_ #>= _).
@@ -2998,14 +3004,16 @@ clpz_expansion(X0 #= Y0, Equal) :-
         phrase(expr_conds(Y0, Y), CsY),
         list_goal(CsX, CondX),
         list_goal(CsY, CondY),
+        no_popcount_t(CsY, YT),
+        no_popcount_t(CsX, XT),
         expansion_simpler(
                 (   CondX ->
-                    (   var(Y) -> Y is X
+                    (   YT, var(Y) -> Y is X
                     ;   CondY -> X =:= Y
                     ;   T is X, clpz:clpz_equal(T, Y0)
                     )
                 ;   CondY ->
-                    (   var(X) -> X is Y
+                    (   XT, var(X) -> X is Y
                     ;   T is Y, clpz:clpz_equal(X0, T)
                     )
                 ;   clpz:clpz_equal(X0, Y0)
-- 
2.54.0