From 7947ffc93066afdf119eadf6a50361ed7522f9e3 Mon Sep 17 00:00:00 2001
From: Florian Renkin <frenkin@lrde.epita.fr>
Date: Thu, 4 Nov 2021 10:20:48 +0100
Subject: [PATCH] ltlsynt: correct verbose when --aiger is used

* bin/ltlsynt.cc: here
* tests/core/ltlsynt.test: add test
---
 bin/ltlsynt.cc          |  2 +-
 tests/core/ltlsynt.test | 21 ++++++++++++++++++++-
 2 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/bin/ltlsynt.cc b/bin/ltlsynt.cc
index a6c172a6b..d32e87fc1 100644
--- a/bin/ltlsynt.cc
+++ b/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";
           }
diff --git a/tests/core/ltlsynt.test b/tests/core/ltlsynt.test
index da93550cc..2d11c58af 100644
--- a/tests/core/ltlsynt.test
+++ b/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
\ No newline at end of file
+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