z3 - 量指定子の下での等式の伝播に関する Z3 の問題

Question

Z3 がタイムアウトする次の簡単な例があります。

(set-option :produce-models true) 
(define-fun T_0 (($in1 Real) ($in2 Real)
  ($out Real) ($assms Bool) ($prop Bool)) Bool 
   (and (= $assms (< $in1 $in2)) 
        (= $prop (=> $assms (and (< $in1 $out) (< $out $in2))))))

(declare-fun $in1$0 () Real)
(declare-fun $in2$0 () Real)
(declare-fun $out$0 () Real)
(declare-fun $assms$0 () Bool)

(assert (forall (($out$0 Real) ($assms$0 Bool)) 
           (not (and (T_0 $in1$0 $in2$0 $out$0 $assms$0 true)))))
(check-sat)

ここで、アサーションを単純化して等価性を伝搬すると、z3 はすぐに UNSAT を返します (予想どおり)。

(define-fun T_1 (($in1 Real) ($in2 Real)
    ($out Real) ($prop Bool)) Bool 
      (and  (= $prop (=> (< $in1 $in2) (and (< $in1 $out) (< $out $in2))))))
(declare-fun $in1$0 () Real)
(declare-fun $in2$0 () Real)
(declare-fun $out$0 () Real)
(assert (forall (($out$0 Real) ($assms$0 Bool)) 
           (not (and (T_1 $in1$0 $in2$0 $out$0 true)))))
(check-sat)

この例は、Z3 が量指定子の下で等式を伝搬しないことを示しているようです。たとえば、次のアサーションは機能します (UNSAT が生成されます)。

 (assert (forall (($out$0 Real)) 
     (and (not (= true (=> (< $in1$0 $in2$0) 
          (and (< $in1$0 $out$0) (< $out$0 $in2$0))))))))

z3 に等式を伝播させる方法、または方程式を使用する別の検索戦略を選択する方法はありますか?