From 8a3a3dc91bf228209615d5c563c7713e47713873 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Mar 2023 15:31:37 -0700 Subject: [PATCH] fix #6648 --- src/sat/smt/pb_internalize.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/pb_internalize.cpp b/src/sat/smt/pb_internalize.cpp index 1a83dbc87ca..17f2bd4ded6 100644 --- a/src/sat/smt/pb_internalize.cpp +++ b/src/sat/smt/pb_internalize.cpp @@ -119,7 +119,7 @@ namespace pb { else { bool_var v = s().add_var(true); literal lit(v, sign); - add_pb_ge(v, sign, wlits, k.get_unsigned()); + add_pb_ge(v, false, wlits, k.get_unsigned()); TRACE("ba", tout << "root: " << root << " lit: " << lit << "\n";); return lit; } @@ -146,7 +146,7 @@ namespace pb { else { sat::bool_var v = s().add_var(true); sat::literal lit(v, sign); - add_pb_ge(v, sign, wlits, k.get_unsigned()); + add_pb_ge(v, false, wlits, k.get_unsigned()); TRACE("goal2sat", tout << "root: " << root << " lit: " << lit << "\n";); return lit; }