Model term without location leads to a failure of the rac prover
With the following code
module Wrong
use bv.BV64 as BV64
lemma wrong: (forall x : BV64.t. BV64.sle x (0x29 : BV64.t))
end
and the command line why3 prove -P CVC4,1.8,counterexamples a.mlw --check-ce
I get the well-known error: anomaly: (Failure "model term has no location")
. Note that I can get a counter-example if I do not turn on the rac-checker.