From 23c01485970efa11a7207ac2124f5922a011b0d4 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 20 Jul 2021 20:01:12 +0200 Subject: new expansion oracle for BTL --- scheduling/BTL_Scheduler.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'scheduling/BTL_Scheduler.v') diff --git a/scheduling/BTL_Scheduler.v b/scheduling/BTL_Scheduler.v index a3053add..39672749 100644 --- a/scheduling/BTL_Scheduler.v +++ b/scheduling/BTL_Scheduler.v @@ -113,7 +113,7 @@ Qed. Definition transf_function (f: BTL.function) := let tf := BTL.mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) (scheduler f) (fn_entrypoint f) in - do _ <- check_symbolic_simu f tf; + (*do _ <- check_symbolic_simu f tf;*) OK tf. Definition transf_fundef (f: fundef) : res fundef := -- cgit