Assertion violation at /src/muz/spacer/spacer_qe_project.cpp:495

[602] % z3 small.smt2
Failed to verify: a.is_numeral(val, r)
ASSERTION VIOLATION
File: ../src/muz/spacer/spacer_qe_project.cpp
Line: 495
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[603] % 
[603] % cat small.smt2
(set-logic HORN)
(set-option :fp.xform.inline_eager false)
(set-option :fp.spacer.native_mbp false)
(set-option :fp.spacer.reach_dnf false)
(declare-fun a (Int Bool Int Bool) Bool)
(declare-fun c (Int Int Bool Bool Int Int Int Int Bool Bool Bool Int Int Bool Bool Int Int Int Int Bool Bool Bool) Bool)
(declare-fun d (Bool Bool Bool Int Bool Int Int Bool Bool Int Int Int Int Bool Bool Bool Int Int Bool Bool Int Int Int Int Bool Bool Bool) Bool)
(declare-fun e (Int Int Bool Bool Int Int Int Int Bool Bool Bool Bool) Bool)
(assert (forall ((ef Int) (eaa Int) (eabacad Bool) (eabacg Bool)) (=> eabacad (a eaa eabacg ef eabacad))))
(assert
 (forall ((no Int)
     (naf Int)
     (nphl Bool)
     (nphiacg Bool)
     (nphq Bool)
     (nphiacad Bool)
     (nrsag Int)
     (nrsah Int)
     (nrst Int)
     (nrsai Int)
     (nrsuacg Bool)
     (nrsv Int)
     (nrsw Int)
     (nrsx Int)
     (nrsaj Int)
     (nrsuacad Bool)
     (nyacad Bool)
     (nzeaa Int)
     (nzeabacg Bool)
     (nzef Int)
     (nzeabacad Bool)
     (nyacg Bool))
 (=> (a nzeaa nzeabacg nzef nzeabacad)
  (c naf nzeaa nzeabacg nyacg nrsag nrsah nrst nrsai nrsuacg nphl nphiacg no nzef
  nzeabacad nyacad nrsv nrsw nrsx nrsaj nrsuacad nphq nphiacad))))
(assert
 (forall ((nak Bool)
     (nal Bool)
     (nam Bool)
     (nphl Bool)
     (nphiacg Bool)
     (ninit_invalid_s Int)
     (nao Bool)
     (nphae Bool)
     (nphiacj Bool)
     (nrsag Int)
     (nrsah Int)
     (nrst Int)
     (nrsai Int)
     (nrsuacg Bool)
     (nap Int)
     (nrsaq Int)
     (nrsar Int)
     (nrsas Int)
     (nrs__synapse_5_x Int)
     (nrsuacj Bool)
     (nyacg Bool)
     (nyacj Bool)
     (naf Int)
     (nat Int)
     (nzeaa Int)
     (nzeabacg Bool)
     (nau Int)
     (nzeav Int)
     (nzeabacj Bool)
     (naw Bool))
 (let ((ax (=> nao (< nap 0 nau))))
  (let ((ay (= naw ax)))
  (=> ay (d nak nal nam ninit_invalid_s naw naf nzeaa nzeabacg nyacg nrsag nrsah nrst nrsai
      nrsuacg nphl nphiacg nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj))))))
(assert
 (forall ((naf Int)
     (nzeaa Int)
     (nzeabacg Bool)
     (nyacg Bool)
     (nrsag Int)
     (nrsah Int)
     (nrst Int)
     (nrsai Int)
     (nrsuacg Bool)
     (nphl Bool)
     (nphiacg Bool)
     (no Int)
     (nzef Int)
     (nzeabacad Bool)
     (nyacad Bool)
     (nrsv Int)
     (nrsw Int)
     (nrsx Int)
     (nrsaj Int)
     (nrsuacad Bool)
     (nphq Bool)
     (nphiacad Bool)
     (nak Bool)
     (nal Bool)
     (nam Bool)
     (ninit_invalid_s Int)
     (naw Bool)
     (nat Int)
     (nzeav Int)
     (nzeabacj Bool)
     (nyacj Bool)
     (nrsaq Int)
     (nrsar Int)
     (nrsas Int)
     (nrs__synapse_5_x Int)
     (nrsuacj Bool)
     (nphae Bool)
     (nphiacj Bool))
 (=> (c naf nzeaa nzeabacg nyacg nrsag nrsah nrst nrsai nrsuacg nphl nphiacg no nzef nzeabacad
    nyacad nrsv nrsw nrsx nrsaj nrsuacad nphq nphiacad)
  (d nak nal nam ninit_invalid_s naw no nzef nzeabacad nyacad nrsv nrsw nrsx nrsaj nrsuacad nphq
  nphiacad nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj)
  (e nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj naw))))
(assert
 (forall ((naw Bool)
     (nat Int)
     (nzeav Int)
     (nzeabacj Bool)
     (nyacj Bool)
     (nrsaq Int)
     (nrsar Int)
     (nrsas Int)
     (nrs__synapse_5_x Int)
     (nrsuacj Bool)
     (nphae Bool)
     (nphiacj Bool))
 (not (e nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj naw))))
(check-sat)
[604] %
OS: Ubuntu 18.04 Commit: cb13641
Z3Prover / z3

Assertion violation at /src/muz/spacer/spacer_qe_project.cpp:495 #3845
