Hello,

While running tests for SYNTCOMP 2019 we found that ltlsynt outputs an incorrect controller on one of our benchmarks:

simple_arbiter_enc_2.tlsf (available from https://bitbucket.org/swenjacobs/syntcomp/src/master/SelectedBenchmarks2018/LTL-TLSF-selection-2018.zip)

I am calling the tool with --aiger --algo=lar and using iimc as our model checker.

Best,

Guillermo