search

zetzit / zz

🍺🐙 ZetZ a zymbolic verifier and tranzpiler to bare metal C
MIT License
1.6k stars 52 forks source link

solvecomp.sh: fedora has yices-smt2 #9

Closed rurban closed 4 years ago

rurban commented 4 years ago

not yices_smt2 I made an alias, and solvecomp.sh works fine now

aep commented 4 years ago

aye, yices_smt2 is probably just available from the in-source builds so using yices-smt2 is probably the better default

rurban commented 4 years ago

And on my debian box I only have yices (version 1.0.36)

aep commented 4 years ago

right, that one won't work. zz should default to z3 in this case.

the script is really only used to compare the two solvers, because there's still tons of optimization work to be done. zz itself will use whatever of the two solvers is available.

aep commented 4 years ago

@rurban btw just seen your comment on HN. could you run the entire ./ci.sh with only z3 and with only yices_smt2 in PATH ? I'm curious to see what difference you get on your machine. on my 32thread ryzen yices is faster in average because z3 has some bad edge cases

https://github.com/Z3Prover/z3/issues/2833

rurban commented 4 years ago

I also have the same ryzen results. yices is about 10x faster there. Still have to compile latest yices on my Intel box