ASSERTION VIOLATION at src/smt/theory_bv.cpp, Line: 951

[zhendongsu]

Commit: e0a066e
OS: Ubuntu 18.04

[555] % for i in $(seq 1 10) ; do z3release small.smt2; done
unsat
unsat
ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 951
UNEXPECTED CODE WAS REACHED.
Z3 4.12.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
unsat
unsat
ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 951
UNEXPECTED CODE WAS REACHED.
Z3 4.12.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
unsat
unsat
ASSERTION VIOLATION
File: ../src/smt/theory_bv.cpp
Line: 951
UNEXPECTED CODE WAS REACHED.
Z3 4.12.2.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new
unsat
[556] % cat small.smt2
(set-option :smt.threads 7)
(define-fun a () Float16 (fp #b1 #b00000 #b0000000011))
(define-fun l () Float16 (fp #b1 #b00000 #b0000000001))
(declare-fun b () Float16)
(declare-fun r () Float16)
(assert (= l (fp.abs b) r (fp.rem a b)))
(check-sat-using ctx-solver-simplify)