equal
deleted
inserted
replaced
107 "--disable-banner", |
107 "--disable-banner", |
108 "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]), |
108 "--max-time=" ^ string_of_int (Real.ceil (Config.get ctxt SMT_Config.timeout))]), |
109 smt_options = [(":produce-proofs", "true")], |
109 smt_options = [(":produce-proofs", "true")], |
110 default_max_relevant = 200 (* FUDGE *), |
110 default_max_relevant = 200 (* FUDGE *), |
111 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" |
111 outcome = on_first_non_unsupported_line (outcome_of "unsat" "sat" |
112 "warning : proof_done: status is still open"), |
112 "(error \"status is not unsat.\")"), |
113 parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), |
113 parse_proof = SOME (K VeriT_Proof_Parse.parse_proof), |
114 replay = NONE } |
114 replay = NONE } |
115 |
115 |
116 (* Z3 *) |
116 (* Z3 *) |
117 |
117 |