mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 11:42:28 +00:00
Code Activity

fix regression in arithmetic resource bound

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2021-06-03 11:41:34 -07:00
parent d2330055e7
commit 0182187296
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lp_settings.h
View file

@ -209,7 +209,7 @@ public:
double harris_feasibility_tolerance { 1e-7 }; // page 179 of Istvan Maros
double ignore_epsilon_of_harris { 10e-5 };
unsigned max_number_of_iterations_with_no_improvements { 2000000 };
unsigned max_total_number_of_iterations { 2000000 };
unsigned max_total_number_of_iterations { 20000000 };
double time_limit; // the maximum time limit of the total run time in seconds
// dual section
double dual_feasibility_tolerance { 1e-7 }; // page 71 of the PhD thesis of Achim Koberstein