Anomaly: model term has no location
Consider the following example:
use int.Int
use array.Init
let f ()
ensures { forall i. result[i] >= 0 }
= init 2 (fun _ -> 2)
If you load it in the IDE, run Alt-Ergo (or CVC4 or Z3) on the goal, and then click on the proof attempt, you get the following crash:
There was an unrecoverable error during treatment of request:
get task(4,false,true)
with exception:
anomaly: Failure("model term has no location")
By the way, the goal is completely unreadable:
goal f'vc :
(let result'unused'unused = 2 in true) /\
(let o = (fun (_:int) -> 2) in
let anonymous'result'unused'unused = o in
2 >= 0 /\
(forall result:array int.
(forall i:int. 0 <= i /\ i < 2 -> result[i] = (o @ i)) /\
length result = 2 ->
(let init'result'unused'unused = result in forall i:int. result[i] >= 0)))