equal
deleted
inserted
replaced
101 "--proof-merge", |
101 "--proof-merge", |
102 "--disable-print-success", |
102 "--disable-print-success", |
103 "--disable-banner", |
103 "--disable-banner", |
104 "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]), |
104 "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT2_Config.timeout))]), |
105 smt_options = [], |
105 smt_options = [], |
106 default_max_relevant = 350 (* FUDGE *), |
106 default_max_relevant = 250 (* FUDGE *), |
107 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"), |
107 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" "warning : proof_done: status is still open"), |
108 parse_proof = SOME VeriT_Proof_Parse.parse_proof, |
108 parse_proof = SOME VeriT_Proof_Parse.parse_proof, |
109 replay = NONE } |
109 replay = NONE } |
110 |
110 |
111 (* Z3 *) |
111 (* Z3 *) |