[bugfix] Fix typo following doublon elimination

Following a bugfix for doublon elimination, doublons are now eliminated
in add_clause, and as such, in case no simplification is made, the
clause without doublons should be used (and not init). This was a typo
missed during the refactoring of doublon elimination.
This commit is contained in:
Guillaume Bury 2017-04-12 19:23:46 +02:00
parent 7e95911dd8
commit 0fe8ded071

View file

@ -768,8 +768,8 @@ module Make
if history = []
then (
(* update order of atoms *)
List.iteri (fun i a -> init.atoms.(i) <- a) atoms;
init
List.iteri (fun i a -> c.atoms.(i) <- a) atoms;
c
)
else make_clause ?tag:init.tag (fresh_name ()) atoms (History (c :: history))
in