From 7e51d9a0630532bf4930c00f7863fff2fab35cd4 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 7 Feb 2024 12:12:57 +0200 Subject: [PATCH] Refactor is_invariant_node in YamlWitness --- src/witness/yamlWitness.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/witness/yamlWitness.ml b/src/witness/yamlWitness.ml index b7ec584dfb..d9d39ccee1 100644 --- a/src/witness/yamlWitness.ml +++ b/src/witness/yamlWitness.ml @@ -201,9 +201,9 @@ struct let is_invariant_node (n : Node.t) = let loc = Node.location n in match n with - | Statement _ when not loc.synthetic && WitnessInvariant.is_invariant_node n -> - not (is_stub_node n) - | _ -> + | Statement _ -> + not loc.synthetic && WitnessInvariant.is_invariant_node n && not (is_stub_node n) + | FunctionEntry _ | Function _ -> (* avoid FunctionEntry/Function, because their locations are not inside the function where asserts could be inserted *) false in