• Sylvain Dailler's avatar
    Why3 counterex: Changing the way counterex value are get from prover. · 86ebcd21
    Sylvain Dailler authored
    This commit solve a problem raised by Mohamed Iguernlala. If provers give
    more values than asked, the results of counterex becomes inconsistent.
    
    We changed the way corresponding terms are associated to counterex value.
    Now we have a map containing the term corresponding to a counterex asked to
    a prover.
    
    * src/core/model_parser.ml
    (construct_name): Takes a string and create a model_name.
    (build_model_rec): Changed to use term_map which allow a name of asked
    counterex to correspond to the term asked.
    
    * src/core/printer.ml
    (printer_mapping): Changed type of queried_terms to store correspondance
    between names and terms.
    (printer_args): Changed initial value of queried_terms accordingly.
    
    * src/core/smtv2.ml
    (print_info_model): This function now returns the map of names to terms.
    (print_prop_decl): Changed variable model_list accordingly.
    86ebcd21
model_parser.ml 16.1 KB