FIXED: CLP(B): Delay BDD restriction until after the instantiation.

This is necessary to actually take the new value into account.

Example:

    ?- sat(A*B>=C*D), A=1,B=0,C=1,D=1.
    false.

This addresses #670.

diff --git a/src/lib/clpb.pl b/src/lib/clpb.pl
index ad49f61c05763ef36a0c70d5f2e8e004af02afee..0b802a462918a44865bede82c4a68fad938f5548 100644 (file)
--- a/src/lib/clpb.pl
+++ b/src/lib/clpb.pl
@@ -842,9 +842,8 @@ verify_attributes(Var, Other, Gs) :-
             (   integer(Other) ->
                 (   between(0, 1, Other) ->
                     root_get_formula_bdd(Root, Sat, BDD0),
-                    bdd_restriction(BDD0, I, Other, BDD),
                     root_put_formula_bdd(Root, Sat, BDD),
-                    Gs = [satisfiable_bdd(BDD)]
+                    Gs = [bdd_restriction(BDD0,I,Other,BDD),satisfiable_bdd(BDD)]
                 ;   no_truth_value(Other)
                 )
             ;   atom(Other) ->