     (queues/pq-add-all! q initial-elements)
     q))
 
-(defn merge-safe 
-  "Merge maps m1 and m2.  If a key is in m1 and m2, the value for m1 will be retained.
-   Moreover, we will assert that (pred m1-val m2-val)."
-  [pred m1 m2]
-  (merge-with (fn [x y] (assert (pred x y)) x) m1 m2))
+(defn assoc-safe [m pred k v]
+  (if (contains? m k) 
+    (do (assert (pred (get m k) v)) m)
+    (assoc m k v)))
 
 ; empty refinement !
 

;; Difficulty: nodes with multiple ancestors.

(defprotocol HasCutoff (cutoff [x]))
(defprotocol HasQueue (queue [x]))

(deftype PartialResult [result-map cutoff]
  HasCutoff (cutoff [] cutoff))

  HasCutoff (cutoff [] (- (second (queues/pq-peek-min queue))))
  HasQueue  (queue [] queue))

;; Represents an action sequence from a state, with sanode representing the first action in remaining-actions.
 ; (or nil, if remaining-actions is empty.)
(deftype SANodeEntry [state sanode reward-to-state remaining-actions]
  Object
   (equals [y] (and (= state (:state y)) (= remaining-actions (:remaining-actions y))))
   (hashCode [] (unchecked-add (int (hash state)) 
                               (unchecked-multiply (int 13) (int (hash remaining-actions))))))


(defn make-queue [initial-elements]
