diff --git a/src/math/lp/lp_settings.h b/src/math/lp/lp_settings.h index 99a7a7b70..456f082c7 100644 --- a/src/math/lp/lp_settings.h +++ b/src/math/lp/lp_settings.h @@ -271,8 +271,8 @@ public: m_int_patch_only_integer_values(true), limit_on_rows_for_hnf_cutter(75), limit_on_columns_for_hnf_cutter(150), - m_enable_hnf(true) - m_print_external_var_name(false), + m_enable_hnf(true), + m_print_external_var_name(false) #ifdef Z3DEBUG , m_counter_for_debug(0) #endif