From 9baa3f0716cddcfbe4daa0d8f7ba4a4def6e6767 Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Mon, 12 Sep 2016 10:38:13 +0200
Subject: [PATCH] fix bug in `add_clause`

---
 src/core/internal.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 7f8ae862..87084022 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -759,7 +759,12 @@ module Make
     try
       let atoms, history = partition init.atoms in
       let clause =
-        if history = [] then init
+        if history = []
+        then (
+          (* update order of atoms *)
+          List.iteri (fun i a -> init.atoms.(i) <- a) atoms;
+          init
+        )
         else make_clause ?tag:init.tag (fresh_name ()) atoms (History (init :: history))
       in
       Log.debugf 4 "New clause:@ @[%a@]" (fun k->k St.pp_clause clause);