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

Merge branch 'master' of github.com:Gbury/mSAT

Browse source
This commit is contained in:
Guillaume Bury 2016-04-15 12:11:38 +02:00
commit ec7c6602e9
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
solver/internal.ml
View file

@ -633,8 +633,6 @@ module Make
| History _ -> assert false
in
try
(* if not force && Proof.has_been_proved init0 then raise Trivial; *)
(* if not (Proof.is_proven init0) then assert false; (* Important side-effect, DO NOT REMOVE *) *)
let atoms, history, level = partition (Vec.to_list init0.atoms) init0.c_level in
let size = List.length atoms in
match atoms with