Assertion violation at src/smt/smt_enode.h:284

[wintered]

[648] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/smt/smt_enode.h
Line: 284
!m_mark2
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[649] % 
[649] % cat small.smt2
(set-logic BV)
(set-option :proof true)
(set-option :trace true)
(set-option :smt.clause_proof true)
(set-option :smt.phase_selection 5)
(set-option :smt.random_seed 1)
(set-option :rewriter.ite_extra_rules true)
(declare-datatypes ((Nat!2078 0)) (((succ2079 (!2080 Nat!2078)) zero2081)))
(declare-fun nmin!249 (Nat!2078 Nat!2078) Nat!2078)
(declare-fun less!231 (Nat!2078 Nat!2078) Bool)
(assert (forall ((n!247 Nat!2078) (m!248 Nat!2078)) (distinct (nmin!249 n!247 m!248) (ite (less!231 n!247 m!248) n!247 m!248))))
(assert (not (forall ((a!393 Nat!2078) (b!394 Nat!2078) (c!395 Nat!2078)) (= (nmin!249 (nmin!249 a!393 (nmin!249 b!394 c!395)) c!395) (nmin!249 a!393 b!394)))))
(check-sat)
[650] %

OS: Ubuntu 18.04
Commit: 0f69783