From 05f1b4dd1a23320fe59f057547d54e728b7a6a34 Mon Sep 17 00:00:00 2001
From: Jakob Rath <git@jakobrath.eu>
Date: Fri, 7 Oct 2022 16:32:56 +0200
Subject: [PATCH] Update note on subsumption (for later)

---
 src/math/polysat/simplify_clause.cpp | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/math/polysat/simplify_clause.cpp b/src/math/polysat/simplify_clause.cpp
index 1e11dd0e3..92464838e 100644
--- a/src/math/polysat/simplify_clause.cpp
+++ b/src/math/polysat/simplify_clause.cpp
@@ -33,10 +33,12 @@ Notes:
             294: v12 + -1*v10 + -1*v0 + -1 == 0  [ l_undef ]
             295: v10 + v0 + 1 <= v12             [ l_undef ]
 
+        292: v10 + v0 + 1 == 0
         294: v10 + v0 + 1 == v12
         295: v10 + v0 + 1 <= v12
 
-        ==> drop 294
+        ==> drop 294 because it implies 295
+        ==> drop 292 because it implies 295
 
 --*/
 #include "math/polysat/solver.h"