From cb279fba2b16b4c9c23114533ba2ef58357f1d70 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 29 May 2022 10:32:05 -0700
Subject: [PATCH] fix sign for binary propagation hints

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_drat.cpp         | 6 +++++-
 src/sat/smt/arith_axioms.cpp | 4 ++--
 src/sat/smt/arith_solver.cpp | 2 +-
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index ba4c543a8..12ce52b19 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -946,6 +946,11 @@ namespace sat {
                 s += 6;
                 return true;
             }
+            if (0 == strncmp(s, "cut", 3)) {
+                h.m_ty = hint_type::cut_h;
+                s += 3;
+                return true;
+            }
             return false;
         };
 
@@ -999,7 +1004,6 @@ namespace sat {
                 return;
             ws();            
         }
-        return;
     }
 
 }
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index f63714fdd..7cb6a05b6 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -238,8 +238,8 @@ namespace arith {
             sat::proof_hint* bound_params = nullptr;
             if (ctx.use_drat()) {
                 bound_params = &m_farkas2;
-                m_farkas2.m_literals[0] = std::make_pair(rational(1), l1);
-                m_farkas2.m_literals[1] = std::make_pair(rational(1), l2);
+                m_farkas2.m_literals[0] = std::make_pair(rational(1), ~l1);
+                m_farkas2.m_literals[1] = std::make_pair(rational(1), ~l2);
             }
             add_clause(l1, l2, bound_params);            
         };
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index 7796585de..acc810120 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -201,7 +201,7 @@ namespace arith {
         if (ctx.use_drat()) {
             ph = &m_farkas2;
             m_farkas2.m_literals[0] = std::make_pair(rational(1), lit1);
-            m_farkas2.m_literals[1] = std::make_pair(rational(1), lit2);
+            m_farkas2.m_literals[1] = std::make_pair(rational(1), ~lit2);
         }
         assign(lit2, m_core, m_eqs, ph); 
         ++m_stats.m_bounds_propagations;