• Sylvain Dailler's avatar
    Why3 altergo counterex - Allowing values to be printed for Altergo · a5d0aa0b
    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
    * 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
alt_ergo.ml 16.9 KB