z3smtcvc4

Truncate Integers Like C in SMT-LIB 2

I'm passing the symbolic output of a symbolic execution engine to Z3 in SMT-LIB 2 format. I need it to truncate integers like they would be in C. So that (assert (= 1 (/ 3 2))) would be SAT.

These formulas might also have floats, so not all divisions should truncate. Just division of ints.

How does one do this?

Solution

  • Integer division is simply called div:

    (assert (= 1 (div 3 2)))
(check-sat)

    This produces:

    sat