From 256e5f43bc46720f766b02a89366d2aa02c5ffe1 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Mon, 3 Jun 2024 13:33:30 +0100 Subject: [PATCH] Fixes 'infinite' loop on concolic assert(0) --- src/concolic/concolic_choice.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/concolic/concolic_choice.ml b/src/concolic/concolic_choice.ml index 1e2849fad..f897c0df4 100644 --- a/src/concolic/concolic_choice.ml +++ b/src/concolic/concolic_choice.ml @@ -124,7 +124,7 @@ let assertion (vb : Concolic_value.V.vbool) = M (fun st -> (Ok (), if no_choice then st else add_pc_to_thread st assert_pc) ) - else M (fun st -> (Error (Assume_fail vb.symbolic), st)) + else M (fun st -> (Error Assert_fail, st)) let trap t = M (fun th -> (Error (Trap t), th))