CODEWITHSUNDEEP
z3
boot4life
boot4life

Reputation: 5314

What is the Z3 option hi_div0?

What does the Z3 option hi_div0 mean? I was unable to find any documentation.

How does that option affect performance and how does it affect semantics?

Upvotes: 1

Views: 86

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

hi_div0 stands for "Hardware Interpretation of Division by zero. When enabled, this means that divison by zero has a concrete value instead of being uninterpreted (and the remainder too). See e.g., bv_rewriter, which defines the values for signed division; the other values are further down in the same file.

Upvotes: 1

Related Questions