QF_LRA_2.smt2

(set-option :print-success true)
(set-logic QF_LRA)
(declare-fun c0 () Bool)
(declare-fun E0 () Bool)
(declare-fun f0 () Bool)
(declare-fun f1 () Bool)
(push 1)
(assert
  (let ((.def_10 (not f0)))
    (let ((.def_9 (not c0)))
      (let ((.def_11 (or .def_9 .def_10)))
        (let ((.def_7 (not f1)))
          (let ((.def_8 (or c0 .def_7)))
            (let ((.def_12 (and .def_8 .def_11)))
  .def_12
)))))))
(check-sat)
(pop 1)
(declare-fun f2 () Bool)
(declare-fun f3 () Bool)
(declare-fun f4 () Bool)
(declare-fun c1 () Bool)
(declare-fun E1 () Bool)
(assert
  (let ((.def_23 (not f2)))
    (let ((.def_20 (= c0 c1)))
      (let ((.def_22 (or E0 .def_20)))
        (let ((.def_24 (or .def_22 .def_23)))
          (let ((.def_18 (not f4)))
            (let ((.def_19 (or c1 .def_18)))
              (let ((.def_25 (and .def_19 .def_24)))
  .def_25
))))))))
(push 1)
(check-sat)
(assert (and f1 (not f1)))
(check-sat)
(pop 1)
(exit)