CODEWITHSUNDEEP
concurrencyz3multicoresmtz3py
Mark Jin
Mark Jin

Reputation: 2903

z3 SMT solver performance on different platforms

I have logic problems written using z3py. I run them on both my pc (intel core i5 + 8GB RAM) and a cluster (32 AMD Operaton 6320 cpus + 500GB RAM). There is no big difference on the runtime and sometimes the remote server takes longer time which confuses me. Does anyone have any idea whether z3 solver is more efficient on multi-core machine?

Upvotes: 1

Views: 818

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

By default, Z3 does not make use of multiple cores or CPUs.

It does however, come with the par-or and par-and tactics which can be used to craft custom tactics that make use of parallelism.

Upvotes: 3

Related Questions