building Cloogle fails
Building Cloogle fails since 17-09. So this is likely caused by cloogle@e75de623. (We need better error reporting to spot such problems earlier. We will take care of this.)
The error message:
./CloogleServer --no-license --rank-settings-constraints rank_settings_constraints.json | tee rank_settings.json
Could not lock memory (12); process may get swapped out
z3 failed to compute a model with these constraints:
(declare-const rs_matching_ngrams_q Real)
(declare-const rs_matching_ngrams_r Real)
(declare-const rs_record_field Real)
(declare-const rs_constructor Real)
(declare-const rs_unifier_n_types Real)
(declare-const rs_unifier_n_funcs Real)
(declare-const rs_unifier_n_conss Real)
(declare-const rs_unifier_n_args Real)
(declare-const rs_resolved_context Real)
(declare-const rs_unresolved_context Real)
(declare-const rs_freevar_context Real)
(declare-const rs_module_usages Real)
(assert (< (+ (* rs_matching_ngrams_q 1) (+ (* rs_matching_ngrams_r 0.6) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.62428209583567)))))))))))) (+ (* rs_matching_ngrams_q 1) (+ (* rs_matching_ngrams_r 0.3) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.52891670027765))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 1) (+ (* rs_matching_ngrams_r 0.5) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0)))))))))))) (+ (* rs_matching_ngrams_q 1) (+ (* rs_matching_ngrams_r 0.333333333333333) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.62428209583567))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 1) (+ (* rs_matching_ngrams_r 0.75) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.46239799789896)))))))))))) (+ (* rs_matching_ngrams_q 0.5) (+ (* rs_matching_ngrams_r 0.3) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 1) (+ (* rs_matching_ngrams_r 0.75) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.46239799789896)))))))))))) (+ (* rs_matching_ngrams_q 0.333333333333333) (+ (* rs_matching_ngrams_r 0.4) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0.9) (+ (* rs_matching_ngrams_r 0.782608695652174) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.698970004336019)))))))))))) (+ (* rs_matching_ngrams_q 0.15) (+ (* rs_matching_ngrams_r 0.5) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.55870857053317))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0.7) (+ (* rs_matching_ngrams_r 0.518518518518518) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.698970004336019)))))))))))) (+ (* rs_matching_ngrams_q 0.15) (+ (* rs_matching_ngrams_r 0.5) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.55870857053317))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0.5) (+ (* rs_matching_ngrams_r 0.588235294117647) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.698970004336019)))))))))))) (+ (* rs_matching_ngrams_q 0.15) (+ (* rs_matching_ngrams_r 0.5) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.55870857053317))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0.75) (+ (* rs_matching_ngrams_r 0.714285714285714) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.698970004336019)))))))))))) (+ (* rs_matching_ngrams_q 0.15) (+ (* rs_matching_ngrams_r 0.5) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.55870857053317))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.52891670027765)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 1) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.62428209583567))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 1) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.62428209583567)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 3) (+ (* rs_unifier_n_funcs 1) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 2.62428209583567))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.62428209583567)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 1.34242268082221))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.62428209583567)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 1.34242268082221)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 1) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.44715803134222))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 2) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.51054501020661)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 2) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 3) (* rs_module_usages 2.51054501020661))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 1) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.54406804435028))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 1) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.54406804435028))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 3) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.845098040014257))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 2) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.51054501020661))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 2) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.51054501020661)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 3) (+ (* rs_unifier_n_args 2) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.63144376901317))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.07918124604762)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 3) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.845098040014257))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.07918124604762))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 2) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 2.50242711998443)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.07918124604762)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.69810054562339))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 2) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.44870631990508)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 1) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.65513843481138))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 1) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 1) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.65513843481138))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 1) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.85125834871908)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 0.954242509439325))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 3) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.845098040014257)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 1) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.65513843481138))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.76342799356294)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 2.55870857053317))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.76342799356294)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 2) (+ (* rs_unifier_n_args 2) (+ (* rs_resolved_context 2) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.54406804435028))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 2.55870857053317)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 2) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 1) (* rs_module_usages 2.44870631990508))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 1.54406804435028)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.845098040014257))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 0) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 1) (* rs_module_usages 1.54406804435028)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 1) (+ (* rs_unifier_n_args 0) (+ (* rs_resolved_context 2) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 1.54406804435028))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 4) (+ (* rs_unifier_n_args 2) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 2) (* rs_module_usages 2.01283722470517)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 3) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 2.53529412004277))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 4) (+ (* rs_unifier_n_args 2) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 2) (* rs_module_usages 2.01283722470517)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 3) (+ (* rs_unifier_n_args 3) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 2.45636603312904))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 1) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 4) (+ (* rs_unifier_n_args 2) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 2) (* rs_module_usages 2.01283722470517)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 3) (+ (* rs_unifier_n_args 3) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 0.845098040014257))))))))))))))
(assert (< (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 2) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 1) (+ (* rs_resolved_context 1) (+ (* rs_unresolved_context 1) (+ (* rs_freevar_context 0) (* rs_module_usages 1.67209785793572)))))))))))) (+ (* rs_matching_ngrams_q 0) (+ (* rs_matching_ngrams_r 0) (+ (* rs_record_field 0) (+ (* rs_constructor 0) (+ (* rs_unifier_n_types 4) (+ (* rs_unifier_n_funcs 0) (+ (* rs_unifier_n_conss 0) (+ (* rs_unifier_n_args 3) (+ (* rs_resolved_context 0) (+ (* rs_unresolved_context 0) (+ (* rs_freevar_context 0) (* rs_module_usages 2.65513843481138))))))))))))))
(set-option :pp.decimal true)
(check-sat)
(get-model)
(exit)