search

rems-project / cerberus

Cerberus C semantics
https://www.cl.cam.ac.uk/~pes20/cerberus/
Other
53 stars 28 forks source link

Specify explicit theory in SMT solver backend #571

Open yav opened 2 months ago

yav commented 2 months ago

There might be performance benefits if we explicitly tell the solver what theories to use.

dc-mak commented 3 weeks ago

We should also add Z3 flags to adjust performance like this: https://github.com/Z3Prover/z3/issues/7352

cp526 commented 3 weeks ago

As of https://github.com/rems-project/cerberus/commit/0ef1e7075079a5befb4d02e8a156e9ad8fcd76c0 CN specifies the logic in the CVC5 backend. It would be easy to add a Z3 setting for the flag mentioned above.