-
Sylvain Dailler authored
We added the generation of identifiers for counterex values inside the printer of altergo. Also added a file to factorize counterex printing functions that are used for both altergo and smtv2. * Makefile.in (cntexmp_printer): Factorization file added to Makefile. * src/driver/parse_smtv2_model_lexer.mll (MODEL): Adding model keyword. * src/driver/parse_smtv2_model_parser.mly (output): Added parsing when keyword model is at beginning of the output of the prover. * src/printer/alt_ergo.ml Adding info mimicking smtv2.ml inside most printing functions for counterex generation. * src/printer/cntexmp_printer.ml Common functions to alt_ergo.ml and smtv2.ml * src/printer/smtv2.ml Removed functions that are factorized into cntexmp_printer.ml
a5d0aa0b