Z3Prover
diff --git a/‎src/math/lp/int_branch.cpp‎
Lines changed: 1 addition & 1 deletion b/‎src/math/lp/int_branch.cpp‎
Lines changed: 1 addition & 1 deletion
diff --git a/‎src/math/lp/int_solver.cpp‎
Lines changed: 1 addition & 1 deletion b/‎src/math/lp/int_solver.cpp‎
Lines changed: 1 addition & 1 deletion
@@ -62,7 +62,7 @@ int int_branch::find_inf_int_base_column() {
     mpq new_range;
     mpq small_value(1024);
     unsigned n = 0;
-    lar_core_solver & lcs = lra.m_mpq_lar_core_solver;
+    lar_core_solver & lcs = lra.get_core_solver();
     unsigned prev_usage = 0; // to quiet down the compiler
     unsigned k = 0;
     unsigned usage;
 
@@ -420,7 +420,7 @@ namespace lp {
 
     int_solver::int_solver(lar_solver& lar_slv) :
         lra(lar_slv),
-        lrac(lra.m_mpq_lar_core_solver) {
+        lrac(lra.get_core_solver()) {
         m_imp = alloc(imp, *this);
         lra.set_int_solver(this);
     }
Original file line number	Diff line number	Diff line change
`@@ -420,7 +420,7 @@ namespace lp {`
`420`	`420`
`421`	`421`	`int_solver::int_solver(lar_solver& lar_slv) :`
`422`	`422`	`lra(lar_slv),`
`423`		`- lrac(lra.m_mpq_lar_core_solver) {`
	`423`	`+ lrac(lra.get_core_solver()) {`
`424`	`424`	`m_imp = alloc(imp, *this);`
`425`	`425`	`lra.set_int_solver(this);`
`426`	`426`	`}`