This program causes the interpreter to behave incorrectly:
rel bar(i32)
rel foo(i32 smt)
rel baz
foo(`#x[?]`).
baz :-
bar(X),
foo(`X`),
X + 1 = 42.
bar(0).
(* Make sure `foo` is recursive in `ok` stratum, so that when `ok` rule is run,
`foo` predicate is reordered to be first *)
foo(`0`) :- baz.
foo(`#x0[?]`).
foo(`#x1[?]`).
foo(`#x2[?]`).
foo(`#x3[?]`).
foo(`#x4[?]`).
foo(`#x5[?]`).
foo(`#x6[?]`).
foo(`#x7[?]`).
foo(`#x8[?]`).
foo(`#x9[?]`).
foo(`#xa[?]`).
foo(`#xb[?]`).
foo(`#xc[?]`).
foo(`#xd[?]`).
foo(`#xe[?]`).
foo(`#xf[?]`).
foo(`41`).
bar(41).
fun len(xs: 'a list): i32 =
match xs with
| [] => 0
| _ :: t => 1 + len(t)
end
rel ok
ok :-
baz,
len(foo(??)) = 19.
Run in semi-naive evaluation mode, it derives only 18 foo facts. Run in eager evaluation mode, it crashes in the baz rule trying to add an SMT variable and a primitive integer.
The problem is that the interpreter currently assigns numeric IDs to solver variables independently of IDs to other terms, so that two different terms (a solver variable and something else) can have the same ID. This breaks assumptions made elsewhere in the interpreter.
This program causes the interpreter to behave incorrectly:
Run in semi-naive evaluation mode, it derives only 18
foofacts. Run in eager evaluation mode, it crashes in thebazrule trying to add an SMT variable and a primitive integer.The problem is that the interpreter currently assigns numeric IDs to solver variables independently of IDs to other terms, so that two different terms (a solver variable and something else) can have the same ID. This breaks assumptions made elsewhere in the interpreter.