From a97e5fcf0ef0d5ca7f69c1276ae5b7b5aeed8666 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 28 Feb 2025 18:18:51 -0800 Subject: [PATCH] fix error in mk_nuget_task.py Signed-off-by: Nikolaj Bjorner --- scripts/mk_nuget_task.py | 2 +- src/math/lp/int_solver.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/scripts/mk_nuget_task.py b/scripts/mk_nuget_task.py index 2dbc8f134..79b14fd6a 100644 --- a/scripts/mk_nuget_task.py +++ b/scripts/mk_nuget_task.py @@ -78,7 +78,7 @@ def unpack(packages, symbols, arch): files = ["Microsoft.Z3.dll", "Microsoft.Z3.pdb", "Microsoft.Z3.xml"] for b in files: file1 = f"{package_dir}/bin/{b}" - file2 = os.path.join(file,"netstandard2.0") + file2 = os.path.join(file1,"netstandard2.0") if os.path.exists(file1): zip_ref.extract(file1, f"{tmp}") replace(f"{tmp}/{package_dir}/bin/{b}", f"out/lib/netstandard2.0/{b}") diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp index f39718c00..9edb3187b 100644 --- a/src/math/lp/int_solver.cpp +++ b/src/math/lp/int_solver.cpp @@ -321,7 +321,7 @@ namespace lp { if (r == lia_move::undef) r = patch_basic_columns(); if (r == lia_move::undef && should_find_cube()) r = int_cube(lia)(); if (r == lia_move::undef) lra.move_non_basic_columns_to_bounds(); - // if (r == lia_move::undef) r = tighten_bounds(); + if (r == lia_move::undef) r = tighten_bounds(); if (r == lia_move::undef && should_hnf_cut()) r = hnf_cut(); if (r == lia_move::undef && should_gomory_cut()) r = gomory(lia).get_gomory_cuts(2); if (r == lia_move::undef && should_solve_dioph_eq()) r = solve_dioph_eq();