(smt.ematching, rewriter.ite_extra_rules, AUFNIRA) Segmentation fault (release) or Assertion violation at ../src/ast/rewriter/bool_rewriter.cpp Line: 655 (debug)

[muchang]

Hi,
For this case, Z3 throws out a segmentation fault:

[669] % z3 small.smt2
Failed to verify: BR_FAILED != try_ite_value(to_app(e), val, result)
ASSERTION VIOLATION
File: ../src/ast/rewriter/bool_rewriter.cpp
Line: 655
UNREACHABLE CODE WAS REACHED.
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[670] % 
[670] % z3release small.smt2
Failed to verify: BR_FAILED != try_ite_value(to_app(e), val, result)
Failed to verify: BR_FAILED != try_ite_value(to_app(t), val, result)
Segmentation fault
[671] % 
[671] % cat small.smt2
(set-logic AUFNIRA)
(set-option :smt.ematching false)
(set-option :rewriter.ite_extra_rules true)
(declare-datatypes ((Nat 0)) (((succ (pred Nat)) (zero))))
(declare-datatypes ((Lst 0)) (((Nil))))
(declare-fun minus (Nat Nat) Nat)
(declare-fun nat-to-int (Nat) Int)
(declare-fun drop (Nat Lst) Lst)
(declare-fun take (Nat Lst) Lst)
(assert (forall ((x Nat) (y Nat)) (=> (= 0 (nat-to-int y)) (= x y))))
(assert (forall ((x Nat) (y Nat)) (= (nat-to-int (minus x y)) (ite (< 0 0) 0 (- 0 (nat-to-int y))))))
(assert (not (forall ((n Nat) (m Nat) (xs Lst)) (= (drop n (take m xs)) (take (minus m n) (drop n xs))))))
(check-sat)
[672] %

OS: Ubuntu 18.04
Commit: 0f69783