Mentions légales du service

Skip to content
  • Sylvain Dailler's avatar
    Q217-025 Allow parsing for reference in counterexamples · f9e2170a
    Sylvain Dailler authored
    Parsing reference was forgotten in commit for Q217-025. This solves the
    problem with a new token MK_ANYTHING.
    
    * src/driver/parse_smtv2_model_lexer.mll
    (parse): Added lexing for all remaining mk*___ record constructs.
    
    * src/driver/parse_smtv2_model_parser.mly
    (smt_term): An smt_term can be a reference to a smt_term. It means it can
    be (Mk_anything smt_term).
    
    Change-Id: Ib529fee83d16d09266e526ca5fb3c65526addff5
    f9e2170a