Why does 'mkInt' take an int as parameter instead of a long (as it is supported by Z3) ?

epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver

Apache License 2.0

122 stars 34 forks source link

Why does 'mkInt' take an int as parameter instead of a long (as it is supported by Z3) ? #49

Closed radustoenescu closed 5 years ago

radustoenescu commented 8 years ago

I have issues working with long values because the provided 'mkInt' function accepts only ints, despite long values being supported by the Z3 java api.

samarion commented 7 years ago

I'm pretty sure you can use mkNumeral(Long.toString(v), mkIntSort()) for this.