• Sylvain Dailler's avatar
    Change the way counterexamples are parsed · 3ea32678
    Sylvain Dailler authored
    The way records are recognized during model parsing is changed:
    we previously recognized records during parsing by looking at the name of
    the variable returned by the prover (mk_r mk__rep etc).
    Now, we collect the names of constructor of records (recognized using
    their id_string beginning with "mk ") during the printing of the smt2
    files. So, after parsing of the model, we can match the name of an
    application with a previously collected constructor: we can recreate
    the record.
    The same can be done for all algebraic datatype.
    This change also solve the problem of parsing in ce-bench.
model_parser.mli 10.6 KB