Slow unsat multiplication overflow solving

[alph6]

Hello.

I've found out that asserting no multiplication overflow is very slow when the answer is unsat. The simplest example I was able to produce is as follows:

(declare-fun a () (_ BitVec 16))
(declare-fun b () (_ BitVec 16))
(declare-fun c () (_ BitVec 16))
(assert (bvugt b a))
(assert (bvugt (bvmul a c) (bvmul b c)))
(assert (bvumul_noovfl a c))
(assert (bvumul_noovfl b c))
(check-sat)

This example takes ~20 seconds to solve on my machine, and I want to be able to work with vectors of length up to 64, so this is too slow for my case.

As mush as I've understood from reading previous questions on this matter and this article, these functions are supposed to be more effective, than simply multiplying extended vectors and checking if the higher half is zero. However, it takes exactly the same amount of time to do so:

(declare-fun a () (_ BitVec 16))
(declare-fun b () (_ BitVec 16))
(declare-fun c () (_ BitVec 16))
(assert (bvugt b a))
(assert (bvugt (bvmul a c) (bvmul b c)))
(assert (= ((_ zero_extend 16) (bvmul a c)) (bvmul ((_ zero_extend 16) a) ((_ zero_extend 16) c))))
(assert (= ((_ zero_extend 16) (bvmul b c)) (bvmul ((_ zero_extend 16) b) ((_ zero_extend 16) c))))
(check-sat)

Following references from aforementioned article to this paper, I tried to implement a more constricting formula (as it is ok in my case to lose some solutions) for no multiplication overflow, checking that the number of significant bits in input operands is at most n. It even works about two times faster, but this is still not enough (which might very well be due to my ineffective design, as I'm unfamiliar with solver internal optimizations).

(declare-fun a () (_ BitVec 16))
(declare-fun b () (_ BitVec 16))
(declare-fun c () (_ BitVec 16))
(assert (bvugt b a))
(assert (bvugt (bvmul a c) (bvmul b c)))
(assert
  (let (
      (a0 (= ((_ extract 0 0) a) #b1))
      (a1 (= ((_ extract 1 1) a) #b1))
      (a2 (= ((_ extract 2 2) a) #b1))
      (a3 (= ((_ extract 3 3) a) #b1))
      (a4 (= ((_ extract 4 4) a) #b1))
      (a5 (= ((_ extract 5 5) a) #b1))
      (a6 (= ((_ extract 6 6) a) #b1))
      (a7 (= ((_ extract 7 7) a) #b1))
      (a8 (= ((_ extract 8 8) a) #b1))
      (a9 (= ((_ extract 9 9) a) #b1))
      (a10 (= ((_ extract 10 10) a) #b1))
      (a11 (= ((_ extract 11 11) a) #b1))
      (a12 (= ((_ extract 12 12) a) #b1))
      (a13 (= ((_ extract 13 13) a) #b1))
      (a14 (= ((_ extract 14 14) a) #b1))
      (a15 (= ((_ extract 15 15) a) #b1))
      (b0 (= ((_ extract 0 0) b) #b1))
      (b1 (= ((_ extract 1 1) b) #b1))
      (b2 (= ((_ extract 2 2) b) #b1))
      (b3 (= ((_ extract 3 3) b) #b1))
      (b4 (= ((_ extract 4 4) b) #b1))
      (b5 (= ((_ extract 5 5) b) #b1))
      (b6 (= ((_ extract 6 6) b) #b1))
      (b7 (= ((_ extract 7 7) b) #b1))
      (b8 (= ((_ extract 8 8) b) #b1))
      (b9 (= ((_ extract 9 9) b) #b1))
      (b10 (= ((_ extract 10 10) b) #b1))
      (b11 (= ((_ extract 11 11) b) #b1))
      (b12 (= ((_ extract 12 12) b) #b1))
      (b13 (= ((_ extract 13 13) b) #b1))
      (b14 (= ((_ extract 14 14) b) #b1))
      (b15 (= ((_ extract 15 15) b) #b1))
      (c0 (= ((_ extract 0 0) c) #b1))
      (c1 (= ((_ extract 1 1) c) #b1))
      (c2 (= ((_ extract 2 2) c) #b1))
      (c3 (= ((_ extract 3 3) c) #b1))
      (c4 (= ((_ extract 4 4) c) #b1))
      (c5 (= ((_ extract 5 5) c) #b1))
      (c6 (= ((_ extract 6 6) c) #b1))
      (c7 (= ((_ extract 7 7) c) #b1))
      (c8 (= ((_ extract 8 8) c) #b1))
      (c9 (= ((_ extract 9 9) c) #b1))
      (c10 (= ((_ extract 10 10) c) #b1))
      (c11 (= ((_ extract 11 11) c) #b1))
      (c12 (= ((_ extract 12 12) c) #b1))
      (c13 (= ((_ extract 13 13) c) #b1))
      (c14 (= ((_ extract 14 14) c) #b1))
      (c15 (= ((_ extract 15 15) c) #b1))
    )
  (and
    (not
      (or
        (and a0 c15)
        (and a1 (or c15 c14))
        (and a2 (or c15 c14 c13))
        (and a3 (or c15 c14 c13 c12))
        (and a4 (or c15 c14 c13 c12 c11))
        (and a5 (or c15 c14 c13 c12 c11 c10))
        (and a6 (or c15 c14 c13 c12 c11 c10 c9))
        (and a7 (or c15 c14 c13 c12 c11 c10 c9 c8))
        (and a8 (or c15 c14 c13 c12 c11 c10 c9 c8 c7))
        (and a9 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6))
        (and a10 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5))
        (and a11 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4))
        (and a12 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3))
        (and a13 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3 c2))
        (and a14 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3 c2 c1))
        (and a15 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3 c2 c1 c0))
      )
    )
    (not
      (or
        (and b0 c15)
        (and b1 (or c15 c14))
        (and b2 (or c15 c14 c13))
        (and b3 (or c15 c14 c13 c12))
        (and b4 (or c15 c14 c13 c12 c11))
        (and b5 (or c15 c14 c13 c12 c11 c10))
        (and b6 (or c15 c14 c13 c12 c11 c10 c9))
        (and b7 (or c15 c14 c13 c12 c11 c10 c9 c8))
        (and b8 (or c15 c14 c13 c12 c11 c10 c9 c8 c7))
        (and b9 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6))
        (and b10 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5))
        (and b11 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4))
        (and b12 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3))
        (and b13 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3 c2))
        (and b14 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3 c2 c1))
        (and b15 (or c15 c14 c13 c12 c11 c10 c9 c8 c7 c6 c5 c4 c3 c2 c1 c0))
      )
    )
  )
  )
)
(check-sat)

The question is, am I missing some important tactic or option, or is it supposed to be that slow?