[SMT-COMP] Is my solver considered a "wrapper tool"?

Delcypher delcypher at gmail.com
Mon Jun 12 13:00:55 EDT 2017


I was reading the definition of a wrapper solver in the current rules
[1] and I'd like to know if my tool is consider as a "wrapper tool".

The definition given is

"A wrapper tool is defined as any solver which calls one or more SMT
solvers not written by the author of the wrapper tool"

I'm not sure if my tool falls under this definition because it is not
specified precisely what is meant by "call".

My tool

* Uses Z3's SMTLIBv2 parser
* Uses Z3's expression language
* Uses some of Z3's tactics in order to do expression simplification

However to solve the constraints Z3 is not used to solve the
simplified expressions (unless a particular command line option is
passed which will not be used for the competition).

I intend to acknowledge Z3 in my system description anyway but I'd
like to know whether I should call my solver a "wrapper tool" or not
in that description.

[1] http://smtcomp.sourceforge.net/2017/rules17.pdf


More information about the SMT-COMP mailing list