(set-option :fp.xform.fix_unbound_vars true)
(declare-fun a (Bool Bool Bool Int Int Int Int Int Int Int Int Int Bool Int Int Int Int Bool) Bool)
(declare-fun b (Bool Bool Bool Int Bool Int Int Int Int Bool Bool Bool Int Int Int Int Bool Bool Bool) Bool)
(assert
 (forall
 ((c Int)
  (d Int)
  (dfabac Bool)
  (dad Bool)
  (dfabg Bool)
  (dh Bool)
  (di Int)
  (dj Bool)
  (dk Bool)
  (dl Int)
  (dm Int)
  (dn Int)
  (do Int)
  (dae Int)
  (dp Int)
  (dq Int)
  (dr Int)
  (ds Int)
  (daf Int))
 (let ((e (and (= dfabac dad) (or (not (= dad true)) (= d dp)))))
  (=> e (a dh dj dk dp dn di do d dae d c dm dfabac daf ds dr dq dfabg)))))
(assert
 (forall
 ((agh Bool)
  (agj Bool)
  (agk Bool)
  (agahuv Bool)
  (agahuwabac Bool)
  (agp Int)
  (agahux Bool)
  (agahuwabg Bool)
  (agaidy Int)
  (agaidae Int)
  (agaidz Int)
  (agaide Int)
  (agaidaj Int)
  (agaidaa Int)
  (agaidak Int)
  (agaidm Int)
  (agaidfabal Bool)
  (agaidfabac Bool)
  (agn Int)
  (agi Int)
  (ago Int)
  (agl Int)
  (agaidaf Int)
  (agaids Int)
  (agaidr Int)
  (agaidq Int)
  (agaidfabg Bool)
  (agam Bool))
 (let ((an (a agh agj agk agp agn agi ago agl agaidy agaidz agaidaj agaidak agaidfabal agaidaf agaids agaidr agaidq agaidfabg)))
  (=> an (b agh agj agk agp agam agaidae agaide agaidaa agaidm agaidfabac agahuv agahuwabac agaidaf agaids agaidr agaidq agaidfabg agahux agahuwabg)))))
(assert
 (forall
 ((agaidy Int)
  (agaidz Int)
  (agaidaj Int)
  (agaidak Int)
  (agaidfabal Bool)
  (agahuao Bool)
  (agahuwabal Bool)
  (agh Bool)
  (agj Bool)
  (agk Bool)
  (agp Int)
  (agam Bool)
  (agaidaf Int)
  (agaids Int)
  (agaidr Int)
  (agaidq Int)
  (agaidfabg Bool)
  (agahux Bool)
  (agahuwabg Bool))
 (not (b agh agj agk agp agam agaidy agaidz agaidaj agaidak agaidfabal agahuao agahuwabal agaidaf agaids agaidr agaidq agaidfabg agahux agahuwabg))))
(check-sat-using horn)

ASSERTION VIOLATION
File: ../src/muz/transforms/dl_mk_rule_inliner.cpp
Line: 428
!has_quantifier(*r.get())
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB