Q:

Wrong result by ":arith.euclidean_solver true"

This smt2 script gives unsat if I use
(check-sat-using (then simplify solve-eqs (repeat bit-blast) (! smt :bv.enable_int2bv true :arith.euclidean_solver true))), and gives sat if I remove :arith.euclidean_solver true. The expected result is sat.
Z3 version 4.4.0
Thank you in advance.

A:

I opened a bug on github to track this.
The URL is: https://github.com/Z3Prover/z3/issues/100

