Mentions légales du service

Skip to content
  • David Hauzar's avatar
    OB10-023 Parse prover output with presence of mk_t__ref. · 772f4fc5
    David Hauzar authored
    Enabling the transformation detect_polymorphism caused some variables be
    of reference type and their values outputed in the form "mk_t__ref value".
    This was not recognized by the counterexample model parser.
    
    * src/driver/parse_smtv2_model_lexer.mll
    Add new token corresponding to string "mk_t__ref"
    
    * src/driver/parse_smtv2_model_parser.mly
    Value can be also of the form "(mk_t__ref value)"
    772f4fc5