Unsoundness in elim_data step for Kodkod reduction.

[hargoniX]

Consider the following problem minimized from Chako:

data Nat :=
  Nat_zero
  | Nat_succ Nat.

rec Nat_add : Nat -> Nat -> Nat :=
  forall (x_0 : Nat) . Nat_add x_0 Nat_zero = x_0;
  forall (x_1 : Nat) . forall (x_2 : Nat) . Nat_add x_1 (Nat_succ x_2) = Nat_succ (Nat_add x_1 x_2).

rec Nat_mul : Nat -> Nat -> Nat :=
  forall (x_3 : Nat) . Nat_mul x_3 Nat_zero = Nat_zero;
  forall (x_4 : Nat) . forall (x_5 : Nat) . Nat_mul x_4 (Nat_succ x_5) = Nat_add (Nat_mul x_4 x_5) x_4.

pred [wf] Std_Commutative : (Nat -> Nat -> Nat) -> prop :=
  forall (x_7 : Nat -> Nat -> Nat) . (forall (x_10 : Nat) . forall (x_11 : Nat) . x_7 x_10 x_11 = x_7 x_11 x_10) => Std_Commutative x_7.

goal ~ (Std_Commutative (fun (x_13 : Nat) . fun (x_14 : Nat) . Nat_mul x_13 x_14)).

After the elim_data pass during the reduction to Kodkod, Nunchaku produces the following definition for Std.Commutative:

  rec Std_Commutative_neg_spec_0- : prop :=
      Std_Commutative_neg_spec_0-  = false.

and thus subsequently comes to the conclusion that Nat_mul is indeed not commutative which is of course false.