Use uninterpreted functions for division

[gustavo-grieco]

SMT bitvector division (bvudiv, bvsdiv, bvurem, bvsrem) is expensive for solvers. Halmos uses uninterpreted functions during symbolic execution, deferring exact division semantics to a refinement phase. This dramatically speeds up path exploration while remaining sound.

[msooseth]

We had a version of this but we removed it. It may be useful for exploration though! Didn’t think of that. We could also just limit the timeout for the solver when it’s running an exploration query? Maybe that’s an easier solution? Modern solvers do this kind of transformation already usually. Now that we can have individual timeouts for queries, this would be a VERY easy thing to do… and may be simpler? Also can be done ALONGSIDE this solution!

…

On Fri, Jan 30, 2026, at 8:55 PM, Gustavo Grieco wrote: *gustavo-grieco* created an issue (argotorg/hevm#995) <#995> SMT bitvector division (`bvudiv`, `bvsdiv`, `bvurem`, `bvsrem`) is expensive for solvers. Halmos uses *uninterpreted functions* during symbolic execution, deferring exact division semantics to a refinement phase. This dramatically speeds up path exploration while remaining sound. — Reply to this email directly, view it on GitHub <#995>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AXYLY5HPKQ5HRFXPJOBL6N34JOZJZAVCNFSM6AAAAACTPG3NF2VHI2DSMVQWIX3LMV43ASLTON2WKOZTHA3TOMJUG44DCOI>. You are receiving this because you are subscribed to this thread.Message ID: ***@***.***>

[gustavo-grieco]

It seems that we need at least some of this for prove_div_negative_divisor and prove_div_values from abdk-math-64.64-verification. Feel free to experiment with these, these takes seconds to get the problematic smt queries and they are not very big.

[blishko]

As Mate said, this would ideally be implemented at the level of the solvers. Bitwuzla should be doing this kind of abstraction internally.
Let's see if we can figure out why they would be struggling on these examples.

[gustavo-grieco]

I'm totally in favor of using bitwuzla infrastructure, if it works as good as our own, and we don't have to maintain additional code. If this is exclusive from bitwuzla, however, we must consider strongly recommend user to use that solver over others. In any case, here are the zip unsolved queries for each abdk invariant related with division:

prove_div_negative_divisor.zip
prove_div_values.zip

I don't know if any configuration of bitwuzla can solve this in a reasonable time. If you want, I can also provide the augmented smts that can be easily solved in seconds using #996.

[gustavo-grieco]

@blishko please check if this zip file contains the abstract arithmetic queries that you need.

prove_div_values_abs.zip

[msooseth]

Note to self

• It takes 5 mins to prove_div_values with the PR, but we get8x -> SMT solver says: Result unknown by SMT solver without it
• The prove_div_negative_divisor is immediate with this PR, and at least a few minutes (probably timeout, I'm lazy) without it.