From 80d34e9f22415ba07c0bdfde2eb817145f923452 Mon Sep 17 00:00:00 2001 From: 2over12 Date: Mon, 13 Jan 2025 13:18:22 -0500 Subject: [PATCH] fix semantics of branching --- .../engine/general_semantics/general/g_interpreter.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml index ea2c36e1e..42d8e3a65 100644 --- a/GillianCore/engine/general_semantics/general/g_interpreter.ml +++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml @@ -857,11 +857,11 @@ struct | Error x -> Right (Exec_err.EState x)) ret in - let b_counter, has_branched = - match successes with - | [] -> (b_counter, false) - | _ -> (b_counter + 1, true) + + let b_counter = + Int.max 0 (List.length successes - 1) + b_counter in + let has_branched = List.length successes > 1 in let spec_name = spec.data.spec_name in let success_confs = successes