              ; linear part
              [:eq f1 [:+ f0 [:* limit dt]]]
              ; quadratic part (we'll use sampling refinement to "switch" it to linear on a subsequent timepoint)
-             (into [:or]
-                   (map (fn [[a b]]
-                          [:and
-                           [:geq flow0 a]
-                           [:leq flow0 b]
-                           ;force dt <= time to reach limit. this means we'll
-                           ; have a self-transition, probably a global self-transition (sampling refinement)
-                           ; todo: could this 'acc-duration' be "until leaving the bin"? Maybe needless since we have the flow1 constraints below.
-                           [:leq dt acc-duration]
-                           ;force flow1 to be within the bin as well, for the same reason
-                           [:geq [:+ flow0 [:* acc dt]] a]
-                           [:leq [:+ flow0 [:* acc dt]] b]
-                           ; actually bound f1 into a box flowpipe
-                           [:geq f1 [:+ f0 [:* a dt]]]
-                           [:leq f1 [:+ f0 [:* b dt]]]])
-                        bins))])))
+             (reduce (fn [else [a b]]
+                       [:ite [:and
+                              [:geq flow0 a]
+                              [:leq flow0 b]]
+                        [:and
+                         ;force dt <= time to reach limit. this means we'll
+                         ; have a self-transition, probably a global self-transition (sampling refinement)
+                         ; todo: could this 'acc-duration' be "until leaving the bin"? Maybe needless since we have the flow1 constraints below.
+                         [:leq dt acc-duration]
+                         ;force flow1 to be within the bin as well, for the same reason
+                         [:geq [:+ flow0 [:* acc dt]] a]
+                         [:leq [:+ flow0 [:* acc dt]] b]
+                         ; actually bound f1 into a box flowpipe
+                         [:geq f1 [:+ f0 [:* a dt]]]
+                         [:leq f1 [:+ f0 [:* b dt]]]]
+                        else])
+                     false
+                     bins)])))
       (vector? flow)
       (let [[acc limit] flow
             dv [:- limit f0]]

                                time-steps edge-states)))]
            [z3 :bound nil])))
      ;todo: could we combine option generation and outcome checking to reduce the calls to the solver? i guess it would make each call a little more expensive since the "take some edge" constraints would be there.
      (let [try-all-options false
            options
            (if try-all-options

             (butlast ts)
             (rest ts))))))

(defn bmc! [{ctx :context :as z3} objects unroll-min unroll-limit target-states]
  (println "unroll" unroll-limit)
  (let [z3 (assert-valuation! z3 objects "t00")
        vars (map (fn [idx]
