                                                      [v (var-name ha-id v "enter" last-t)])
                                                    vars))
                                 _ (assert (not (empty? v0-vars)))
+                                mid-t (var-name "mid-t" new-t last-t)
+                                vmid-vars (into {}
+                                                (map (fn [v] [v (var-name ha-id v "check" last-t)])
+                                                     vars))
                                 vT-vars (into {}
                                               (map (fn [v] [v (var-name ha-id v "exit" last-t)])
                                                    vars))

                                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

                  :tr-caches  tr-caches
                  :inputs     #{}}
          check-may-first? true
          ;todo: the performance on this model checking is nowhere near good enough. If I could get formula generation sped up then maybe it would be worth considering, but even running the solver at a depth of 15 or 16 takes over a second.
          ;todo: try running just bmc-1! and push/assert-reached/pop each time.
          [may-status may-witness] (if check-may-first?
                                     (let [[may-status may-witness]
                                           (time (with-solver
                                                   (assoc z3 :must-semantics? false)
                                                   (fn [z3]
                                                     (rest (bmc! z3 (:objects config) 0 unroll-limit target-states)))))]
                                       (if (= may-status :witness)
                                         [may-status may-witness]
                                         [:unsat nil]))
                                     [:skipped nil])
          start-depth (max 0 (dec (count may-witness)))]
      (if (or (= may-status :skipped)
              (= may-status :witness))
        (ha/spy "checked must"
                (time (with-solver
                        (assoc z3 :must-semantics? true)
                        (fn [z3]
                          (println "check must at" start-depth ".." unroll-limit)
                          (let [[z3 status all-steps] (time (bmc! z3 (:objects config) start-depth unroll-limit target-states))]
                            (println "check result:" status all-steps)
                            (if (= status :witness)
                              (let [moves-per-t (map
                                                  (fn [[tprev tprevval _mprev]
                                                       [tnext tnextval mnext]]
                                                    [[tprev tprevval] [tnext tnextval] mnext])
                                                  (butlast (concat [["t00" 0 nil]]
                                                                   all-steps))
                                                  all-steps)]
                                (fipp/pprint ["rollout" moves-per-t] {:print-level 6})
                                [:witness moves-per-t])
                              [:unsat nil]))))))
        [:unsat nil]))
    (catch Exception e
      (println "Error!")
