Precondition Invariant: Disjunct over matching state invariants #786

Merged

sim642 merged 18 commits intoyaml-witness-preconditionfrom

yaml-witness-precondition-groups

Aug 4, 2022

Commits on Jul 14, 2022

Add example where the generated witnesses are unsound.
jerhard
committed

Commits on Jul 19, 2022

Commits on Jul 22, 2022

Use start state instead of context for generating preconditions
jerhard
committed

Commits on Jul 25, 2022

Commits on Jul 26, 2022

Explicitely use BatHashtbl instead of doing it via Prelude.Hashtbl.
jerhard
committed
Move comment about why we do not generate invariants for FunctionEntry and Function(-return) nodes to is_invariant_node
jerhard
committed

Commits on Jul 27, 2022