So the empty solver needs to be installed?

That's my concern. This would work for nix users, but if someone just wants to use hevm's executable they would have to set the empty solver up manually, which I don't think is the right approach.

I very much want to have the empty solver reside in our haskell code. We may need to modify how we interact with the solvers, but I hope that it is doable.

Well, I thought this would be used mostly for debug purposes, so regular users wouldn't need to have to use it. All solvers currently need to be installed, so I thought it would be fine.

We could make this part of hevm, but it would require quite a bit of changes to Solvers.hs, making it less intuitive. Or maybe we can keep sort-of as-is, but then we would require rearchitecting the way Solvers.hs makes use of solvers. I am not against either, I just thought it's cleaner this way. But if we want to advise users to use the empty solver, then indeed we'd need a better solution.

I am not convinced that we should advise users to use empty -- it can't get solutions for address expressions or jump expressions, and it cannot help with most if then else branches -- so hevm is likely to behave very differently with empty than without: different (not just more or less -- but different) SMT2 queries will be dispatched. The solver is used quite extensively during exploration, not only during solving.

Put this way I agree with you.

@gustavo-grieco, how are you running hevm actually? Do you use Nix?

BTW, we can move the empty solver to hevm codebase. So it'd be built when hevm is built. Not sure that helps, but we can definitely do that.

Unless it is part of hevm library, it would probably not improve the situation, right?
I agree that the solution I would like to have would require changes in the architecture around solvers.
If the Nix solution works for Gustavo, I would be OK with it.
If I ever get to have enough time, I would look at the Solvers.hs architecture.

If it is only for debugging, advanced user can install it manually even if they are not using nix. Let's proceed then.