Performance bottleneck in clause minimization

[arbimo]

The following flatzinc model shows pathological performance entirely due to the minimize_clause function.

The problem seem to be that the integer variables see thousands of bound updates due to propagation (expected).
This triggers an edge case where minimize_clause may be quadratic in the size of the trail because it needs to lookup the entailing event of each encountered literal.

just samply aries_fzn grocery.fzn  # assuming the content below is in this file

% Generated by MiniZinc 2.9.2
% Solver library: /home/tseraud/Documents/aries/aries_fzn/share/aries
% Command line invocation: minizinc --compile --solver aries grocery2.mzn 

predicate int_lin_le(array [int] of int: as,array [int] of var int: bs,int: c);
predicate int_lin_eq(array [int] of int: as,array [int] of var int: bs,int: c);
array [1..2] of int: X_INTRODUCED_0_ = [1,-1];
array [1..4] of int: X_INTRODUCED_1_ = [1,1,1,1];
var 1..711: A:: output_var;
var 1..711: B:: output_var;
var 1..711: C:: output_var;
var 1..711: D:: output_var;
var 1..505521: X_INTRODUCED_3_ ::var_is_introduced :: is_defined_var; % T1
var 1..505521: X_INTRODUCED_4_ ::var_is_introduced :: is_defined_var; % T2
var 528000000..528000000: X_INTRODUCED_5_ ::var_is_introduced :: is_defined_var; % PRODUIT = 7.11 * 100^4  MODIFIED to 5.28 to fit in INT_CST_MAX
constraint int_lin_le(X_INTRODUCED_0_,[A,B],0); % A <= B
constraint int_lin_le(X_INTRODUCED_0_,[B,C],0); % B <= C
constraint int_lin_le(X_INTRODUCED_0_,[C,D],0); % C <= D
constraint int_lin_eq(X_INTRODUCED_1_,[C,B,A,D],711); % A + B + C + D = 711
constraint int_times(A,B,X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_); % T1 = A * B
constraint int_times(C,D,X_INTRODUCED_4_):: defines_var(X_INTRODUCED_4_); % T2 = C * D
constraint int_times(X_INTRODUCED_3_,X_INTRODUCED_4_,X_INTRODUCED_5_):: defines_var(X_INTRODUCED_5_); % PRODUIT = T1 * T2
solve :: int_search([A,B,C,D,X_INTRODUCED_3_,X_INTRODUCED_4_],first_fail,indomain_min,complete) satisfy;