(smt.phase_selection=0, rlimit=630, rewriter.cache_all, qe2) Assertion violation at ../src/qe/qe_arith.cpp Line: 348

[muchang]

Hi,
For this formula:

(set-option :smt.phase_selection 0)
(set-option :rlimit 630)
(set-option :rewriter.cache_all true)
(assert (forall ((a Int) (b Int)) (exists ((x Int)) (< a (* 20 x) b))))
(check-sat-using qe2)

Z3 throws out an assertion violation:

Failed to verify: a.is_numeral(val, r)
ASSERTION VIOLATION
File: ../src/qe/qe_arith.cpp
Line: 348
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

OS: Ubuntu 18.04
Commit: 18bb90f