Looks similar to #3749 but should be different according to -v:10 output,
[781] % z3 rewriter.flat=false smt.arith.solver=6 small.smt2
Segmentation fault
[782] %
[782] % cat small.smt2
(assert (forall ((?a Int) (?b Int) (?c Int)) (= (* (* ?a ?b) ?c) (* ?a (* ?b ?c)))))
(assert (exists ((?a Int) (?b Int) (?c Int)) (= ?a (* (* ?a ?b) ?c))))
(assert (forall ((?b Real)) (= 0 ?b)))
(assert (forall ((?a Int) (?b Int) (?c Int)) (= (* ?a (* ?b ?c)) (* ?b (* ?a ?c)))))
(check-sat)
[783] %
OS: Ubuntu 18.04
Commit: 121a6de
Looks similar to #3749 but should be different according to
-v:10output,OS: Ubuntu 18.04
Commit: 121a6de