simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-09 20:55:39 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

fix(proof.check): ensure that the proof is an empty clause

Browse source
This commit is contained in:
Simon Cruanes 2019-02-16 12:16:19 -06:00 • committed by Guillaume Bury
parent 92ca9c328f
commit 2e2bbfd4d0
1 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/core/Internal.ml
View file

@ -712,7 +712,11 @@ module Make(Plugin : PLUGIN)
Stack.push (Enter p) s; Stack.push (Enter p) s;
fold_aux s h f acc fold_aux s h f acc
let check p = fold (fun () _ -> ()) () p let check (p:t) =
if Array.length p.atoms > 0 then (
error_res_f "@[<2>Proof.check: non empty conclusion for claus@ %a@]" Clause.debug p;
);
fold (fun () _ -> ()) () p
end end
type proof = Proof.t type proof = Proof.t