From 0fe8ded071f8621f679d9a2972363cc6162fefdf Mon Sep 17 00:00:00 2001 From: Guillaume Bury Date: Wed, 12 Apr 2017 19:23:46 +0200 Subject: [PATCH] [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. --- src/core/internal.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/core/internal.ml b/src/core/internal.ml index 1129fed9..ea488bf1 100644 --- a/src/core/internal.ml +++ b/src/core/internal.ml @@ -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