       (let [flow0 (get v0-vars flow)
             dflow (get flows flow)]
         (cond
+          ;todo: fix nonlinearity by binning
           (= dflow 0) [:eq f1 [:+ f0 [:* flow0 dt]]]
           (vector? dflow)
           (let [[acc limit] dflow

            [:eq f1 [:+ f0 [:* acc dt]]]
            [:leq dt [:/ dv acc]]]]
          ; max
          [:and
           [:implies f0-not-at-limit [:eq f1 [:+ f0 [:* acc dt]]]]
           [:implies [:not f0-not-at-limit] [:eq f1 limit]]])))))

(defn nonlinear-predicate [_z3 x-ha x-flows x-var t]
  (let [vx (get x-flows x-var 0)

            dv [:- limit f0]
            f0-not-at-limit [acc-rel [:+ f0 [:* acc dt]] limit]]
        (if must-semantics?
          ;todo: fix nonlinearity by binning? need to constrain acceleration to a number different from limit
          [:ite [:and [:geq dv (- heval/precision)] [:leq dv heval/precision]]
           ; limit part
           [:eq f1 f0]
           ; accelerating part (don't continue past limit!)
