From 845f5f89e199500ed353d1135c1b9642af7439b4 Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 1 Feb 2023 16:44:52 +0100 Subject: [PATCH] compile --- src/sat/smt/bv_polysat.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/smt/bv_polysat.cpp b/src/sat/smt/bv_polysat.cpp index 1345dde6a..151fc7d55 100644 --- a/src/sat/smt/bv_polysat.cpp +++ b/src/sat/smt/bv_polysat.cpp @@ -147,7 +147,7 @@ namespace bv { for (expr* arg : *a) { expr_ref b2b(m); b2b = bv.mk_bit2bool(a, i); - sat::literal bit_i = ctx.internalize(b2b, false, false, m_is_redundant); + sat::literal bit_i = ctx.internalize(b2b, false, false); sat::literal lit = expr2literal(arg); add_equiv(lit, bit_i); ctx.add_aux_equiv(lit, bit_i);