64 provers = provers, type_enc = type_enc, sound = true, |
64 provers = provers, type_enc = type_enc, sound = true, |
65 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), |
65 lam_trans = lam_trans, relevance_thresholds = (1.01, 1.01), |
66 max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, |
66 max_relevant = SOME (length facts), max_mono_iters = max_mono_iters, |
67 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
67 max_new_mono_instances = max_new_mono_instances, isar_proof = isar_proof, |
68 isar_shrink_factor = isar_shrink_factor, slice = false, |
68 isar_shrink_factor = isar_shrink_factor, slice = false, |
69 timeout = timeout, preplay_timeout = preplay_timeout, expect = ""} |
69 minimize = SOME false, timeout = timeout, |
|
70 preplay_timeout = preplay_timeout, expect = ""} |
70 val problem = |
71 val problem = |
71 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
72 {state = state, goal = goal, subgoal = i, subgoal_count = n, |
72 facts = facts, smt_filter = NONE} |
73 facts = facts, smt_filter = NONE} |
73 val result as {outcome, used_facts, run_time, ...} = |
74 val result as {outcome, used_facts, run_time, ...} = |
74 prover params (K (K (K ""))) problem |
75 prover params (K (K (K ""))) problem |