From a03d7f6bef03088a8bebc2588d73f34ba1389d63 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Tue, 20 Jul 2021 23:30:51 -0400 Subject: [PATCH] fix --- src/sat/Solver.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/Solver.ml b/src/sat/Solver.ml index 7f981cbc..43d9fddc 100644 --- a/src/sat/Solver.ml +++ b/src/sat/Solver.ml @@ -1455,7 +1455,7 @@ module Make(Plugin : PLUGIN) let[@inline never] flush_clauses_ st = while not @@ Vec.is_empty st.clauses_to_add do - let c = Vec.pop st.clauses_to_add in + let c = Vec.pop_exn st.clauses_to_add in add_clause_ st c done @@ -1746,7 +1746,7 @@ module Make(Plugin : PLUGIN) Vec.sort v (fun c1 c2 -> compare c2.activity c1.activity); let n_collected = ref 0 in while Vec.size v > n_of_learnts do - let c = Vec.pop v in + let c = Vec.pop_exn v in assert (Clause.removable c); Clause.set_dead c; assert (Clause.dead c);