equal
deleted
inserted
replaced
77 |
77 |
78 val default_output_dir: Path = Path.explode("dump") |
78 val default_output_dir: Path = Path.explode("dump") |
79 |
79 |
80 def make_options(options: Options, aspects: List[Aspect]): Options = |
80 def make_options(options: Options, aspects: List[Aspect]): Options = |
81 { |
81 { |
82 val options1 = options + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0" |
82 val options0 = if (NUMA.enabled) NUMA.policy_options(options) else options |
|
83 val options1 = options0 + "completion_limit=0" + "ML_statistics=false" + "parallel_proofs=0" |
83 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) |
84 (options1 /: aspects)({ case (opts, aspect) => (opts /: aspect.options)(_ + _) }) |
84 } |
85 } |
85 |
86 |
86 def dump(options: Options, logic: String, |
87 def dump(options: Options, logic: String, |
87 aspects: List[Aspect] = Nil, |
88 aspects: List[Aspect] = Nil, |