Z3 Configuration Enhancements

draperlaboratory / cbat_tools

Program analysis tools developed at Draper on the CBAT project.

MIT License

101 stars 14 forks source link

Z3 Configuration Enhancements #159

Open philzook58 opened 4 years ago

philzook58 commented 4 years ago

Some possible things to investigate whether they can improve Z3 queries

Add debug flag #136
mk_solver instead of mk_simple_solver
Tactics, solver configurations, parallel flags
Presolve arrays, limit arrays sizes

Projects doing similar analysis:

https://github.com/klee/klee/issues/836
https://github.com/klee/klee/pull/659
https://github.com/esbmc/esbmc/issues/32

philzook58 commented 4 years ago

I've found that on the n-queens example, outputting the smtlib2 query and using the z3 command line tool is significantly faster. ~20 seconds -> fractions of a second. This is even after replacing mk_simple_solver with mk_solver. The verbose z3 output seems to be showing roughly the same tactics being applied with identical :num-exprs, but with different memory usage.