https://github.com/uuverifiers/uppsat
Tip revision: 3a2476a13d72278ba1c696e5f655455e3ac4c2ab authored by Peter Backeman on 13 April 2021, 07:37:37 UTC
Add timeout-check at z3 solver result
Add timeout-check at z3 solver result
Tip revision: 3a2476a
todo.org
* What to do with fixedpoint...
* Theoretical:
** Find inclusion bounds for fixed-point
** Analyse what sized models are usually needed
** Ponder about increasing width and maximum width an relation...
* Practical:
** Investigate bounds a bit more.
** Make cactus plot
** Pick 2 bit-widths, and for each bit-width 3 increments
*** Run through (100?) benchmarks
*** Compare with Z3, MathSAT, CVC4(?)
** What about the theory of fixed-point proposed. Can we use it?
