Assertion violation on QF_ANIA formula at theory_arith_core.h:3484 (unsat_core, rlimit, rewriter.flat false, rewriter.eq2ineq, smt.arith.solver 5)

[rainoftime]

Hi, for the following formula, z3 (commit 18bb90f) throws an assertion violation

(set-logic QF_ANIA)
(set-option :unsat_core true)
(set-option :rlimit 397)
(set-option :rewriter.flat false)
(set-option :rewriter.eq2ineq true)
(set-option :smt.arith.solver 5)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i2 Int)
(declare-const v6 Bool)
(declare-const v46 Bool)
(assert (! (or true (distinct 72 72) true v46 true true true) :named IP_57))
(push 1)
(assert (! (= true (<= (mod 662 (- 81 i0 57)) (- i2 i1 81)) true v46 v6 false false false false) :named IP_58))
(check-sat)

ASSERTION VIOLATION
File: ../src/smt/theory_arith_core.h
Line: 3484
lazy_pivoting_lvl() != 0 || m_columns[v].size() == 1
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB

[NikolajBjorner]

not worth it: in the destructor