Obsolete nodes unsoundly reattached after errors
Here are reproduction steps for the bug initially reported by @filliatr in lineardecision.mlw
After recovering from an error, the nodes that became detached due to the error are reattached. However, this reattaches some nodes that were obsolete before that, which is unsound.
Reproduction steps using the example below:
- Prove this file
- Uncomment the precondition of f, reload (the proofs of f,g,h are now obsolete)
- Prove f, but not g or h (leaving them obsolete)
- Uncomment the precondition of g, reload (there is an error because "<" is unknown in B)
- Uncomment the "use import int.Int" in module B, reload
The proof of g is correctly still obsolete, but the proof of h has been reattached but is false (the precondition of f cannot be proved).
module A
use import int.Int
let f (x:int) : int
requires { true (* /\ x < 42*) }
ensures { result = 42 }
= 42
end
module B
use A
(* use import int.Int *)
let g (x:int) : int
requires { true (* /\ x < 42 *) }
ensures { result = 42 }
= A.f x
end
module C
use A
let h (x:int) : int
requires { true }
ensures { result = 42 }
= A.f x
end