warning when cloning module containing only "val"s as abstract symbols
When cloning a module where all abstract symbols are val, like
module A0
val f () : unit
end
module A1
let f () = ()
clone A0 with val f = f
end
Why3 sends the warning cloned theory .A0 does not contain any abstract symbol; it should be used instead
. However, A0
does contain an abstract symbol.