Assertion violation at sat/sat_model_converter.cpp:149

[wintered]

[767] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/sat/sat_model_converter.cpp
Line: 149
sat || undef
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[768] % 
[768] % cat small.smt2
(set-option :sat.xor.solver true)
(declare-fun a () (_ BitVec 8))
(declare-fun b () (_ BitVec 8))
(declare-fun c () (_ BitVec 8))
(declare-fun d () (_ BitVec 8))
(declare-fun e () (_ BitVec 8))
(declare-fun f () (_ BitVec 8))
(declare-fun j () (_ BitVec 8))
(declare-fun g () (_ BitVec 8))
(declare-fun h () (_ BitVec 8))
(assert (bvuge (bvlshr ((_ zero_extend 24) h) ((_ zero_extend 24) (_ bv2 8))) (_ bv8 32)))
(assert (distinct ((_ zero_extend 24) g) (_ bv0 32)))
(assert (let ((?d ((_ zero_extend 24) b))
       (?j ((_ zero_extend 24) c))
       (?i ((_ zero_extend 24) j))
       (?l ((_ zero_extend 24) g))
       (?aa ((_ zero_extend 24) h)))
     (bvult
     (bvadd (_ bv616 32) (bvmul (_ bv4294967295 32) (bvadd ?aa ?l ?i ?j ?d (_ bv9 32))))
     (_ bv256 32))))
(assert (let ((?am ((_ zero_extend 24) a))
       (?j ((_ zero_extend 24) c))
       (?an ((_ zero_extend 24) d))
       (?ao ((_ zero_extend 24) e))
       (?ap ((_ zero_extend 24) f)))
     (distinct (bvadd ?ap ?ao ?an ?j ?am) (_ bv0 32))))
(check-sat)
[769] %

OS: Ubuntu 18.04
Commit: db9d6d1

[zhendongsu]

Nikolaj, you closed this bug report without a fix or comment, so I assume it is of no/little interest, but can you please clarify for us so that we could try to avoid reporting similar issues? Thank you.