Closed ryzhyk closed 10 years ago
Done in synthesis algorithm. It now takes an extra argument to specify what to print. The top level app should provide a way to set this extra argument.
The TSL compiler still outputs unneeded debugging info.
Added --verbose command line option. Disable debug messages in tsl compiler.
I think, we basically want some progress indication by default (e.g., on every refinement) and error reporting. Everything else can be re-enabled by the -v option.