• David Hauzar's avatar
    Query cvc4 for reason of answer unknown and use it for counterexamples. · 5c3038bf
    David Hauzar authored
    When resource limit is hit, cvc4 outputs useless counterexample. Query
    cvc4 for the reason of answer unknown and use the answer to decide
    whether resource limit was hit. If it was hit, do not display the
    counterexample.
    
    * src/driver/call_provers.{ml|mli}
    (parse_prover_run): If the prover answers unknown, get the information
    about the reason of this answer.
    
    * src/printer/smtv2.ml
    (print_prop_decl): Query solver for the reason of answer unknown.
    
    * src/driver/driver.ml
    (load_driver): Initialize Unknown with no information about the reason
    of answer unknown.
    
    * src/session/session.ml
    (load_result): Initialize Unknown with no information about the reason
    of answer unknown.
    
    * src/session/session_scheduler.ml
    (schedule_proof_attempt)
    (edit_proof): Initialize Unknown with no information about the reason
    of answer unknown.
    
    * src/why3session/why3session_lib.ml
    (filter_spec): Initialize Unknown with no information about the reason
    of answer unknown.
    5c3038bf
session_scheduler.ml 35.2 KB