mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 09:34:08 +00:00
remove more warnings
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
552a504f72
commit
8aeba62802
|
@ -177,7 +177,6 @@ namespace lp {
|
|||
for (unsigned i = 0; i < n_of_rows; i++) {
|
||||
auto & row = lra.get_row(i);
|
||||
TRACE("dioph_eq", tout << "row "<< i <<":"; lia.display_row_info(tout, i) << "\n";);
|
||||
unsigned basic_var = lra.r_basis()[i];
|
||||
if (!all_vars_are_int_and_small(row)) {
|
||||
TRACE("dioph_eq", tout << "not all vars are int and small\n";);
|
||||
continue;
|
||||
|
@ -768,7 +767,7 @@ namespace lp {
|
|||
}
|
||||
};
|
||||
// Constructor definition
|
||||
dioph_eq::dioph_eq(int_solver& lia): lia(lia) {
|
||||
dioph_eq::dioph_eq(int_solver& lia) {
|
||||
m_imp = alloc(imp, lia, lia.lra);
|
||||
}
|
||||
dioph_eq::~dioph_eq() {
|
||||
|
|
|
@ -24,7 +24,6 @@ namespace lp {
|
|||
class int_solver;
|
||||
class dioph_eq {
|
||||
class imp;
|
||||
int_solver& lia;
|
||||
imp* m_imp;
|
||||
public:
|
||||
dioph_eq(int_solver& lia);
|
||||
|
|
Loading…
Reference in a new issue