simon/sidekick
1
0
Fork 0
mirror of https://github.com/c-cube/sidekick.git synced 2025-12-06 11:15:43 -05:00
Code Issues Projects Releases Packages Wiki Activity Actions

spurious assertion

Browse source
This commit is contained in:
Simon Cruanes 2016-07-22 16:51:45 +02:00
parent 895cb9cbfb
commit c4beb7054b
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/core/internal.ml
View file

@ -1243,7 +1243,6 @@ module Make
(* Clear hypothesis not valid anymore *) (* Clear hypothesis not valid anymore *)
for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do for i = ul.ul_clauses to Vec.size env.clauses_hyps - 1 do
let c = Vec.get env.clauses_hyps i in let c = Vec.get env.clauses_hyps i in
assert c.attached;
assert (c.c_level > l); assert (c.c_level > l);
detach_clause c detach_clause c
done; done;