(assert
 (forall ((a.k Bool)
     (a.b Bool)
     (a.c Bool)
     (a.d (_ BitVec 8))
     (a.e Bool)
     (a.f Bool)
     (a.aa Bool)
     (a.g Bool))
 (exists ((a.h Bool)
      (a.i (_ BitVec 8))
      (a.j Bool)
      (a.l Bool)
      (a.m (_ BitVec 10))
      (a.n Bool)
      (a.o Bool)
      (a.p (_ BitVec 8))
      (a.q (_ BitVec 8))
      (a.r Bool)
      (a.s Bool)
      (a.t Bool)
      (a.ab (_ BitVec 10))
      (a.ac Bool)
      (a.ad Bool)
      (a.ae Bool)
      (a.af Bool)
      (a.ag Bool)
      (a.ah (_ BitVec 8))
      (a.ai (_ BitVec 8))
      (a.aj Bool)
      (ak (_ BitVec 4))
      (a.al Bool))
  (=> (= a.aa (ite (= a.k false) a.c (ite (= a.k true) true (ite (= a.k false) (ite (not a.b) false a.c) a.c))))
  (and (= a.p (ite a.l (ite (not (ite a.j true a.h)) a.q a.i) a.i))
   (= a.ab (ite a.g (ite (bvugt ((_ zero_extend 22) a.m) (_ bv104 32)) (_ bv0 10) (bvadd (_ bv1 10))) a.m))
   (= a.ah (ite a.t (ite (not (ite a.r true a.o)) a.ai a.p) a.p))
   (= a.aj
   (= a.al
    (ite a.s (ite (or (not a.ag)) true (ite a.t (ite (not (ite a.r true a.o)) false true) a.ae))
    (ite a.n
     (ite (bvugt ((_ zero_extend 22) a.ab) (_ bv104 32))
     (ite (= a.af true) false
      (ite (= a.af true) (= ((_ extract 7 7) a.p) (_ bv1 1))
      (ite (= a.af false) (= ((_ extract 6 6) a.p) (_ bv1 1))
       (ite (= a.af true) (= ((_ extract 5 5) a.p) (_ bv1 1))
       (ite (= a.af false) (= ((_ extract 4 4) a.p) (_ bv1 1))
        (ite (= a.af true) (= ((_ extract 3 3) a.p) (_ bv1 1))
        (ite (= a.af false) (= ((_ extract 2 2) a.p) (_ bv1 1))
         (ite (= a.af true) (= ((_ extract 1 1) a.p) (_ bv1 1))
         (ite (= a.af false) (= ((_ extract 0 0) a.p) (_ bv1 1))
          (ite (= a.af false) true true)))))))))) true) true))
    (= a.ac a.e a.ad) a.f (= a.d a.ah))))))))
(check-sat-using bv)

ASSERTION VIOLATION
File: ../src/tactic/ufbv/ufbv_rewriter.cpp
Line: 689
rewrite(np)==np
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB