ltlsynt: correct verbose when --aiger is used

* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: add test

bin/ltlsynt.cc

@@ -496,7 +496,7 @@ namespace
           {
             *gi->verbose_stream << "AIG circuit was created in "
                                << gi->bv->aig_time
-                               << " and has " << saig->num_latches()
+                               << " seconds and has " << saig->num_latches()
                                << " latches and "
                                << saig->num_gates() << " gates\n";
           }

tests/core/ltlsynt.test

@@ -633,4 +633,23 @@ minimization took X seconds
 EOF
 ltlsynt -f "Fa <-> FGb" --outs=b,c --verbose --decompose=0 --verify 2> out
 sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
-diff outx exp
+diff outx exp
+
+# Test verbose aiger
+
+cat >exp <<EOF
+trying to create strategy directly for Ga <-> Gb
+direct strategy might exist but was not found.
+translating formula done in X seconds
+automaton has 4 states and 1 colors
+LAR construction done in X seconds
+DPA has 4 states, 4 colors
+split inputs and outputs done in X seconds
+automaton has 9 states
+solving game with acceptance: parity max odd 6
+game solved in X seconds
+AIG circuit was created in X seconds and has 0 latches and 0 gates
+EOF
+ltlsynt -f "Ga <-> Gb" --outs=b --verbose --decompose=0 --verify --aiger 2> out
+sed 's/ [0-9.e-]* seconds/ X seconds/g' out > outx
+diff outx exp