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);