What if my tool does not compile on the StarExec platform?

The SYNTCOMP team will work together with tool developers to ensure that all tools run as intended on the platform. If you have reason to doubt that your tool will compile on our servers, consider uploading and testing a first version as soon as possible, such that there is enough time to work on any compilation issues before the competition.

How are synthesized circuits checked for correctness?

AIGER files produced by synthesis tools are checked automatically with a model checker. We will use a separate timeout for model checking (and results that cannot be verified are considered incorrect). In the safety (AIGER) track, synthesis tools can alternatively also produce the winning region of the system, which is then checked for correctness. 

Can I withdraw my tool description if I “lose” the competition?

Tools can only be withdrawn before the actual competition. We will however allow every participating team to react to the competition results by inspecting the behavior of their tools on the benchmarks used in the competition. If bad performance in the competition is due to bugs that can be found and possibly fixed before presentation of the results or publication of the descriptions, the organizers will work together with the developers to shed light on these issues.