fix normalisation of pure expressions

Signed-off-by: Sacha Ayoun <[email protected]>
GillianPlatform · Dec 12, 2023 · 74860c3 · 74860c3
1 parent 1cfebe5
commit 74860c3
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/GillianCore/engine/Abstraction/Normaliser.ml b/GillianCore/engine/Abstraction/Normaliser.ml
@@ -291,6 +291,7 @@ module Make (SPState : PState.S) = struct
       | SetMem (le1, le2) -> SetMem (fe le1, fe le2)
       | ForAll (bt, a) -> ForAll (bt, fant a)
       | IsInt e -> IsInt (fe e)
+      | Impl (a, b) -> Impl (fa a, fa b)
       | _ ->
           let msg =
             Fmt.str