                 limit-part [:* limit limit-duration]]
             (if must-semantics?
               ; sampling refinement.
-              [:ite [:eq flow0 limit]
+              [:ite [:and [:geq dv (- heval/precision)] [:leq dv heval/precision]]
                ; linear part
-               [:eq f1 [:+ f0 [:* flow0 dt]]]
+               [:eq f1 [:+ f0 [:* limit dt]]]
+               ;todo: fix nonlinearity by binning?
                ; quadratic part. force dt <= time to reach limit. this means we'll
                ; have a self-transition, probably a global self-transition.
                [:and
                 [:eq f1 [:+ f0 [:* flow0 dt] [:* acc dt dt]]]
                 [:leq dt acc-duration]]]
               [:ite [flow-rel [:+ flow0 [:* acc dt]] limit]
+               ;todo: fix nonlinearity by binning?
                ;all quadratic
                [:eq f1 [:+ f0 [:* flow0 dt] [:* acc dt dt]]]
                ;average quadratic part, then add linear part

                                     (single-jump-constraints z3 ha-type ha-id in-state (:edges state-def) out-edge vT-vars next-vars last-t new-t)))
                                 has))
            (println "try" opt-edges-by-ha-id)
            (let [cur-model (check! z3)
                  symx-result (if (not-model? cur-model)
                                [z3 :unsat nil]
                                ; else, result = recurse with a decremented bound and the last path constraints
                                (symx!- z3
                                        (dec bound)
                                        target-states
                                        (conj time-steps new-t)
                                        (ha/spy "new path" (conj edge-states opt-edges-by-ha-id))))]
              (pop! z3)
              (if (= (second symx-result) :witness)
                (reduced symx-result)

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