#### The one place for your designs

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.

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
```

To enable design management, you'll need to meet the requirements. If you need help, reach out to our support team for assistance.