add bitwuzla as a solver - #740
Conversation
2d32d03 to
426961f
Compare
|
Any idea why the tests are failing? looks like some odd Circle/CI hassle? The new solver doesn't look like it should affect the existing tests at all? |
| = [ "(set-option :auto-config false)" | ||
| , "(set-option :model true)" ] | ||
| , "(set-option :model true)" | ||
| , "(set-option :sat.smt true)" ] |
There was a problem hiding this comment.
I thought we were told not to use this.
There was a problem hiding this comment.
circle ci is using an ancient version of z3, 4.8.7, released in 2019. That's probably why adding this line causes it to fail. For the gh one, you need to update the cache action. Also, why do you have both circle ci and gh actions running?
There was a problem hiding this comment.
Oh whoops - I did not mean to push that. That is stuff I usually add locally so that tock-veri-asm checks faster. I'll patch it now.
There was a problem hiding this comment.
The GitHub z3's version is also a tiny bit old (4.10.2 released in 2022)
|
@vrindisbacher -- did this bitwuzla thing help? should we try to merge this? |
|
Honestly I haven't had time to take a look. Maybe something to close for now and we can come back to it? |
3 participants
Adding bitwuzla as a solver because it's supposedly good at bitvectory stuff!