equal
deleted
inserted
replaced
531 |> the_default preplay_timeout_default |
531 |> the_default preplay_timeout_default |
532 val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" |
532 val sh_minimizeLST = available_parameter args sh_minimizeK "minimize" |
533 val max_new_mono_instancesLST = |
533 val max_new_mono_instancesLST = |
534 available_parameter args max_new_mono_instancesK max_new_mono_instancesK |
534 available_parameter args max_new_mono_instancesK max_new_mono_instancesK |
535 val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK |
535 val max_mono_itersLST = available_parameter args max_mono_itersK max_mono_itersK |
536 val hard_timeout = SOME (2 * timeout) |
536 val hard_timeout = SOME (4 * timeout) |
537 val (msg, result) = |
537 val (msg, result) = |
538 run_sh prover_name prover type_enc strict max_facts slice lam_trans |
538 run_sh prover_name prover type_enc strict max_facts slice lam_trans |
539 uncurried_aliases e_selection_heuristic term_order force_sos |
539 uncurried_aliases e_selection_heuristic term_order force_sos |
540 hard_timeout timeout preplay_timeout sh_minimizeLST |
540 hard_timeout timeout preplay_timeout sh_minimizeLST |
541 max_new_mono_instancesLST max_mono_itersLST dir pos st |
541 max_new_mono_instancesLST max_mono_itersLST dir pos st |