Wrong result of z3 datalog with predict

[DerZc]

Hi,

Consider the following program:

Z 64

fbnd(A:Z) printtuples
szra(A:Z) input

szra(1).

fbnd(F) :- szra(F), 72 != F, 97 = F.

As there is only one fact in szra and not equals to 97, so the result should be empty.
But I run the program and get the result:

Tuples in fbnd: 
        (A=97(1))
Time: 0ms
Parsing: 0ms, other: 0ms

If I remove the 72 != F in the rule, it will become fbnd(F) :- szra(F), 97 = F.. The result will become:

Tuples in fbnd: 
Time: 0ms
Parsing: 0ms, other: 0ms

But both of these two results should be same and equal to empty.
The version of z3 is cbc5b1f.

[NikolajBjorner]

you are hitting functionality that nobody else exercised in 10 years. I don't have bandwidth to go through such functionality. The other use cases for the datalog engine have been to associate unique strings with identifiers. I have fixed #6446 but will punt on other reports.

Given that z3 is open source you and others are of course invited to fix such bugs.

[DerZc]

Thanks for fixing #6446 and the clarification! We still stop testing Z3's Datalog functionality assuming that this functionality is not actively used, even though we believe to have found other likely unreported bugs. Let us know in case you want us to resume our testing efforts in the future.