Hi,
For this formula:
(simplify (^ (/ (^ 22.0 (/ 3.0 5.0))) 0))
Z3 throws out an assertion violation:
[595] % z3-4.8.7 small.smt2
1.0
[596] % z3 small.smt2
ASSERTION VIOLATION
File: ../src/ast/rewriter/arith_rewriter.cpp
Line: 1171
num_y.is_pos()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
a
[597] %
[597] % cat small.smt2
(simplify (^ (/ (^ 22.0 (/ 3.0 5.0))) 0))
[598] %
OS: Ubuntu 18.04
Commit: a51d65d