Skip to content

Commit

Permalink
Fix inverted condition
Browse files Browse the repository at this point in the history
  • Loading branch information
bclement-ocp committed Jan 22, 2024
1 parent c1a1ee4 commit 0378d9c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/lib/reasoners/satml.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1409,7 +1409,7 @@ module Make (Th : Theory.S) : SAT_ML with type th = Th.t = struct
Note that if the [fuip] is itself a semantic literal, it will act as
a (local) learned clause (see [semantic_expansion]). *)
let has_split = Vec.exists is_semantic lclause.atoms in
if has_split then (
if not has_split then (
Vec.push env.learnts lclause;
attach_clause env lclause;
clause_bump_activity env lclause
Expand Down

0 comments on commit 0378d9c

Please sign in to comment.