From d2f79b1f2b8b9667ab7a69c6da236bf34eb92868 Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Tue, 15 Jan 2019 18:30:48 +0100 Subject: [PATCH] Fix stack overflow in model checking --- src/main.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/main.ml b/src/main.ml index 952a69e1..87a2ce7c 100644 --- a/src/main.ml +++ b/src/main.ml @@ -37,13 +37,13 @@ module Make let check_model state = let check_clause c = - let l = List.map (function a -> + let l = List.rev_map (function a -> Log.debugf 99 "Checking value of %a" (fun k -> k S.St.pp_atom (S.St.add_atom a)); state.Solver_intf.eval a) c in List.exists (fun x -> x) l in - let l = List.map check_clause !hyps in + let l = List.rev_map check_clause !hyps in List.for_all (fun x -> x) l let prove ~assumptions =