[Question] How can I find the usage of Ultimate IntBlastingWrapper?

[merlinsun]

Greetings,

I apologize for submitting this question to the issue tracker.

I recently came across your new work titled “A Bit-vector to Integer Translation with bv2nat and nat2bv” and “Ultimate IntBlastingWrapper.” I find it very interesting and would like to try it out if it’s available. However, I haven’t been able to find any instructions on how to use it in Ultimate or SMTInterpol.

Could you please provide some guidance or direct me to any available instructions?

Thank you very much.

Best regards,

[jhoenicke]

I can speak for SMTInterpol. @Heizmann knows better the status of Ultimate.

The BV support in SMTInterpol based on nat2bv and bv2nat is now merged to master. I haven't done a new release yet, but I can make it if you're interested. Otherwise you can just compile the latest version from the git repository yourself.

It's still relatively new. I think it should be complete, except for multiplication which may cause a benchmark to return unknown. Logical operators are blasted and this may be slow for large bitvector sizes. Multiplication is never blasted and may cause incompleteness.

[merlinsun]

Thank you, @jhoenicke !
That's very helpful. I will try out the latest version of SMTInterpol. I also look forward to hearing more about your great work in the future.
Thanks again for your kind help.