ASSERTION VIOLATION with z3 version 4.13.3.0

[etiennejf]

An assertion violation is randomly obtained when invoking z3 on the following example:

(set-option :print-success true)
(set-logic ALL)
(set-option :produce-models true)
(set-option :produce-proofs true)
(set-option :smt.pull-nested-quantifiers true)
(set-option :smt.mbqi true)
(define-sort Nat () Int)
(define-fun @isNat ((@x Nat)) Bool (<= 0 @x))
(declare-const x Nat)
(declare-const y Nat)
(declare-const z Nat)
(define-fun Nat.mod ((@x Nat)(@y Nat)) Nat (ite (= 0 @y) @x (mod @x @y)))
(assert (not (=> (@isNat x) (=> (@isNat y) (=> (@isNat z) (= (Nat.mod x y) (Nat.mod (+ x (* y z)) y)))))))
(check-sat)

The violation obtained is the following:

ASSERTION VIOLATION
File: /builddir/build/BUILD/z3-z3-4.13.3/src/nlsat/nlsat_solver.cpp
Line: 2770
Failed to verify: m_cache.mk_unique(p) == p

4.13.3.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

Note that this violation is not always obtained systematically on a specific run. Indeed, sometimes a run may return the expected unsat result.