library(clpb) is currently available in SICStus (original version), and SWI (by mat). Let me come to the essence quite rapidly:
?- X = 1+1, sat(X), X = 1+1.
X = 1+1.
?- sat(X), X = 1+1.
false.
So this is a similar problem as it exists in the default state of library(clpfd).
What to do in such a situation?
Update: In library(clpfd) of mat, there is now the functor # /1 for this purpose. Ideally, accompanied with an operator declaration op(150,fx,#), we now can write:
?- X = 1+1, #X #= Y.
ERROR: Type error: `integer' expected, found `1+1' (a compound)
To ensure full algebraic properties one has to declare:
:- set_prolog_flag(clpfd_monotonic, true).
Now, variables that are left ambiguous (thus, being either integers only, or expressions) produce instantiation errors:
?- 1 + 1 #= Y.
ERROR: Arguments are not sufficiently instantiated
?- 1 + 1 #= #Y.
Y = 2.
What to do in such a situation?
In the meantime, also library(clpb) ensures monotonicity similar to library(clpz)/library(clfd). Within this execution mode, explicit variables have to be decorated with (v)/1.
?- current_prolog_flag(clpb_monotonic,B).
B = false. % the default
?- sat(X).
X = 1.
?- set_prolog_flag(clpb_monotonic,true).
true.
?- sat(X).
ERROR: Arguments are not sufficiently instantiated
?- sat(v(X)).
X = 1.
In Scryer, say:
?- use_module(library(clpb)).
true.
?- asserta(clpb:monotonic).
true.
?- sat(X).
error(instantiation_error,instantiation_error(unknown(_67),1)).
?- sat(v(X)).
X = 1.