Z3 FiniteDomain doesn't seem to work with implications

Question

Here's a Z3 program, that creates two variables X and Y which cannot be equal, and have a domain of size 2:

var solver = ctx.MkSolver();

// Section A
var T = ctx.MkFiniteDomainSort("T", 2);
var a = ctx.MkNumeral(0, T);
var b = ctx.MkNumeral(1, T);
var x = ctx.MkConst("x", T);
var y = ctx.MkConst("y", T);

// Section B
//var a = ctx.MkInt(0);
//var b = ctx.MkInt(1);
//var x = ctx.MkIntConst("x");
//var y = ctx.MkIntConst("y");
//solver.Add(ctx.MkLe(a, x), ctx.MkLe(x, b));
//solver.Add(ctx.MkLe(a, y), ctx.MkLe(y, b));

// Section C
//solver.Assert(!ctx.MkEq(x, y));

// Section D
solver.Assert(ctx.MkImplies(ctx.MkEq(x, a), ctx.MkEq(y, b)));
solver.Assert(ctx.MkImplies(ctx.MkEq(x, b), ctx.MkEq(y, a)));
solver.Assert(ctx.MkImplies(ctx.MkEq(y, a), ctx.MkEq(x, b)));
solver.Assert(ctx.MkImplies(ctx.MkEq(y, b), ctx.MkEq(x, a)));

// Section E
//solver.Assert(ctx.MkEq(x, a));

var status = solver.Check();
Console.WriteLine(status);
Console.WriteLine(solver.Model);
Console.WriteLine(solver.Model.Eval(ctx.MkEq(x, a)));
Console.WriteLine(solver.Model.Eval(ctx.MkEq(y, b)));

// Should always be true, but doesn't work when only sections A and D are uncommented?
Console.WriteLine(solver.Model.Eval(ctx.MkImplies(ctx.MkEq(x, a), ctx.MkEq(y, b))));

I get output.

SATISFIABLE
(define-fun y () T
  0)
(define-fun x () T
  0)
true
false
false

This model clearly does not satisfy the constraints. I explicitly evaluate the 1st constraint to double check, and indeed, it's false.

The same problem does not occur if I use integers (section B instead of section A), or I add additional constraints (section C & E).

What am I missing? I'd like to use FiniteDomain as it's more convenient than adding bounds to integers, but it seems it behaves quite differently.

Answer 1

This GitHub issue explains that FiniteDomain is only intended for the Datalog engine, and is broken in other uses.

Using enumerations is the correct way to do this in Z3 in other engines.