Skip to content

Commit a0bac48

Browse files
committed
CHC: limit interception of main assumption to api assumptions
1 parent aada3a5 commit a0bac48

1 file changed

Lines changed: 4 additions & 1 deletion

File tree

CodeHawk/CHC/cchanalyze/cCHPOQuery.ml

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -644,7 +644,10 @@ object (self)
644644
(expl:string) =
645645
if self#env#get_functionname = "main"
646646
&& (match (status, deps) with
647-
| (Green, DEnvC _) -> true | _ -> false) then
647+
| (Green, DEnvC (_, al)) ->
648+
List.exists (fun a ->
649+
match a with ApiAssumption _ -> true | _ -> false) al
650+
| _ -> false) then
648651
self#record_main_api_proof_result ~site status deps expl
649652
else
650653
begin

0 commit comments

Comments
 (0)