mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

fix the crash

Browse source
This commit is contained in:
Lev Nachmanson 2024-08-15 18:18:22 -10:00 • committed by Lev Nachmanson
parent abf29b57aa
commit 3b22d3b19d
4 changed files with 12 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

9
src/math/lp/dioph_eq.cpp
View file

@ -4,8 +4,9 @@
#include "math/lp/lp_utils.h"
namespace lp {
struct imp {
class dioph_eq::imp {
public:
int_solver& lia;
lar_solver& lra;
@ -13,9 +14,9 @@ namespace lp {
vector<lar_term> m_e;
void init() {
int n_of_rows = lra.r_basis().size();
unsigned n_of_rows = static_cast<unsigned>(lra.r_basis().size());
unsigned skipped = 0;
for (unsigned i = 0; i < lra.r_basis().size(); i++) {
for (unsigned i = 0; i < n_of_rows; i++) {
auto & row = lra.get_row(i);
lar_term t;
bool is_int = true;

3
src/math/lp/dioph_eq.h
View file

@ -19,9 +19,10 @@ Revision History:
#include "math/lp/lia_move.h"
namespace lp {
struct imp;
class int_solver;
class dioph_eq {
class imp;
int_solver& lia;
imp* m_imp;
public:

3
src/math/lp/int_solver.cpp
View file

@ -29,7 +29,8 @@ namespace lp {
};
struct imp {
class int_solver::imp {
public:
int_solver& lia;
lar_solver& lra;
lar_core_solver& lrac;

5
src/math/lp/int_solver.h
View file

@ -31,16 +31,17 @@ Revision History:
namespace lp {
class lar_solver;
class lar_core_solver;
struct imp;
class int_solver {
friend struct create_cut;
friend class gomory;
friend class int_cube;
friend class int_branch;
friend class int_gcd_test;
friend class hnf_cutter;
friend struct imp;
friend class imp;
friend class dioph_eq;
class imp;
lar_solver& lra;
lar_core_solver& lrac;
imp* m_imp;