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

Fixed refreshing of clauses with push/pop

Browse source
This commit is contained in:
Guillaume Bury 2016-01-30 17:03:14 +01:00
parent cb8092af3b
commit 30842da947
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/internal.ml
View file

@ -1097,7 +1097,7 @@ module Make
if c.c_level > l then begin if c.c_level > l then begin
remove_clause c; remove_clause c;
match c.cpremise with match c.cpremise with
| History [ { cpremise = Lemma _ } as c' ] -> Stack.push c' s | History ({ cpremise = Lemma _ } as c' :: _ ) -> Stack.push c' s
| _ -> () (* Only simplified clauses can have a level > 0 *) | _ -> () (* Only simplified clauses can have a level > 0 *)
end else begin end else begin
Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c); Log.debugf 15 "Keeping intact clause %a" (fun k->k St.pp_clause c);