mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix 6800
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
50717fb655
commit
51df7b75ce
|
@ -538,6 +538,8 @@ namespace seq {
|
|||
expr_ref t_eq_empty = mk_eq_empty(t);
|
||||
expr_ref xsy = mk_concat(x, s, y);
|
||||
|
||||
verbose_stream() << s << " " << t << "\n";
|
||||
// add_clause(~mk_eq(t, s), i_eq_0);
|
||||
add_clause(cnt, i_eq_m1);
|
||||
add_clause(~t_eq_empty, s_eq_empty, i_eq_m1);
|
||||
add_clause(~s_eq_empty, mk_eq(i, mk_len(t)));
|
||||
|
|
|
@ -31,7 +31,7 @@ namespace lp {
|
|||
lra.remove_fixed_vars_from_base();
|
||||
lp_assert(lia.is_feasible());
|
||||
for (unsigned j : lra.r_basis())
|
||||
if (!lra.get_value(j).is_int())
|
||||
if (!lra.get_value(j).is_int() && lra.column_is_int(j))
|
||||
patch_basic_column(j);
|
||||
if (!lia.has_inf_int()) {
|
||||
lia.settings().stats().m_patches_success++;
|
||||
|
|
Loading…
Reference in a new issue