[537] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/tactic/goal.cpp
Line: 308
!m().proofs_enabled()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[538] % 
[538] % cat small.smt2
(set-logic HORN)
(set-option :fp.xform.scale true)
(set-option :rewriter.arith_lhs true)
(set-option :fp.xform.magic true)
(set-option :fp.spacer.gpdr true)
(set-option :fp.spacer.iuc.old_hyp_reducer true)
(declare-fun P (Real Real Real Real Real Real Real Real Real Real Real
        Real Real Real Real Real Real Real Real Real Real Real
        Real Real Real Real Real Real Real Real Real Real Bool
        Bool Bool Bool Bool Bool Bool Bool Real Real Real Real
        Real Real Real) Bool)
(assert (forall ((a Real)
         (aa Real)
         (b Real)
         (c Real)
         (d Real)
         (ab Real)
         (e Real)
         (f Real)
         (ac Real)
         (ad Real)
         (ae Real)
         (g Real)
         (af Real)
         (h Real)
         (i Real)
         (ag Real)
         (ah Real)
         (j Real)
         (k Real)
         (l Real)
         (ai Real)
         (m Real)
         (aj Real)
         (n Real)
         (o Real)
         (ak Real)
         (p Real)
         (q Real)
         (r Real)
         (al Real)
         (s Real)
         (am Real)
         (an Real)
         (ao Real)
         (ap Real)
         (aq Bool)
         (t Bool)
         (ar Bool)
         (u Bool)
         (v Bool)
         (w Bool)
         (x Bool)
         (as Bool)
         (y Real)
         (z Real)
         (cv Real)
         (at Real))
     (let ((au (and (= a 0) (not (= ap 0)) aq)))
     (=> au (P aa b c d ab e f ac ad ae g af h i ag ah j k l ai m aj n o ak p q r al s am an aq t ar u v w x as y z cv at a ao ap)))))
(assert
 (forall ((aa Real)
     (b Real)
     (c Real)
     (d Real)
     (ab Real)
     (e Real)
     (f Real)
     (ac Real)
     (ad Real)
     (ae Real)
     (g Real)
     (af Real)
     (h Real)
     (i Real)
     (ag Real)
     (ah Real)
     (j Real)
     (k Real)
     (l Real)
     (ai Real)
     (m Real)
     (aj Real)
     (n Real)
     (o Real)
     (ak Real)
     (p Real)
     (q Real)
     (r Real)
     (al Real)
     (s Real)
     (am Real)
     (an Real)
     (aq Bool)
     (t Bool)
     (ar Bool)
     (u Bool)
     (v Bool)
     (w Bool)
     (x Bool)
     (as Bool)
     (y Real)
     (z Real)
     (cv Real)
     (at Real)
     (a Real)
     (ao Real)
     (ap Real)
     (av Real)
     (aw Real)
     (ax Real)
     (ay Real)
     (az Real)
     (ba Real)
     (bb Real)
     (bc Real)
     (bd Real)
     (be Real)
     (bf Real)
     (bg Real)
     (bh Real)
     (bi Real)
     (bj Real)
     (bk Real)
     (bl Real)
     (bm Real)
     (bn Real)
     (bo Real)
     (bp Real)
     (bq Real)
     (br Real)
     (bs Real)
     (bt Real)
     (bu Real)
     (bv Real)
     (bw Real)
     (bx Real)
     (by Real)
     (bz Real)
     (ca Real)
     (cb Real)
     (cc Real)
     (cd Real)
     (ce Bool)
     (cf Bool)
     (cg Bool)
     (ch Bool)
     (ci Bool)
     (cj Bool)
     (ck Bool)
     (cl Bool)
     (cm Real)
     (cn Real)
     (co Real)
     (cp Real))
 (let ((cq (= bj bm ap))
      (cr (= bm 0))
      (cs (= bm ah)))
  (let ((ct (or (and cq cr) (and (= a 2) cs))))
  (=> (P aa b c d ab e f ac ad ae g af h i ag ah j k l ai m aj n o ak p q r al s am an aq t ar u v w x as y z cv at a ao ap)
   (= aw ap)
   ct
   (P ax ay az ba bb bc bd be bf bg bh bi bj bk bl bm bo bp bq br bs bt bu bv bw bx by bz ca cb cc cd ce cf cg ch ci cj ck cl cm cn co cp bn av aw))))))
(assert
 (forall ((aa Real)
     (b Real)
     (c Real)
     (d Real)
     (e Real)
     (f Real)
     (ac Real)
     (ad Real)
     (g Real)
     (h Real)
     (i Real)
     (ag Real)
     (ah Real)
     (j Real)
     (k Real)
     (l Real)
     (ai Real)
     (m Real)
     (aj Real)
     (n Real)
     (o Real)
     (ak Real)
     (p Real)
     (q Real)
     (r Real)
     (al Real)
     (s Real)
     (am Real)
     (an Real)
     (aq Bool)
     (t Bool)
     (ar Bool)
     (u Bool)
     (v Bool)
     (w Bool)
     (x Bool)
     (as Bool)
     (y Real)
     (z Real)
     (cv Real)
     (at Real)
     (a Real)
     (ao Real)
     (ap Real))
 (let ((cu (not (< a 3))))
  (=> (P aa b c d b e f ac ad e g f h i ag ah j k l ai m aj n o ak p q r al s am an aq t ar u v w x as y z cv at a ao ap) cu false))))
(check-