test/regress/regress1/quantifiers/issue4021-ind-opts.smt2

   1 (set-logic ALL)
   2 (set-option :ag-miniscope-quant true)
   3 (set-option :conjecture-gen true)
   4 (set-option :int-wf-ind true)
   5 (set-option :quant-model-ee true)
   6 (set-option :sygus-inference true)
   7 (set-option :uf-ho true)
   8 (set-info :status unsat)
   9 (declare-fun a () Real)
  10 (declare-fun b () Real)
  11 (declare-fun c () Real)
  12 (declare-fun e () Real)
  13 (assert (forall ((d Real)) (and (or (< (/ (* (- a) d) 0) c) (> b 0.0)) (= (= d 0) (= e 0)))))
  14 (check-sat)