From afaf4413775ff7d6054a5893f1397ad908e0773c Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 1 Apr 2021 09:18:27 -0700
Subject: [PATCH] kinds: Remove non-existent properties. (#6253)

---
 src/theory/bags/kinds     | 4 ++--
 src/theory/mktheorytraits | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index cd53484eb..dd8eacfb5 100644
--- a/src/theory/bags/kinds
+++ b/src/theory/bags/kinds
@@ -12,7 +12,7 @@ rewriter ::CVC5::theory::bags::BagsRewriter \
     "theory/bags/bags_rewriter.h"
 
 properties parametric
-properties check propagate presolve
+properties check presolve
 
 # constants
 constant EMPTYBAG \
@@ -90,4 +90,4 @@ typerule BAG_TO_SET          ::CVC5::theory::bags::ToSetTypeRule
 construle UNION_DISJOINT     ::CVC5::theory::bags::BinaryOperatorTypeRule
 construle MK_BAG             ::CVC5::theory::bags::MkBagTypeRule
 
-endtheory
\ No newline at end of file
+endtheory
diff --git a/src/theory/mktheorytraits b/src/theory/mktheorytraits
index 81e551a10..b2c6e1ef2 100755
--- a/src/theory/mktheorytraits
+++ b/src/theory/mktheorytraits
@@ -172,7 +172,7 @@ struct TheoryTraits<${theory_id}> {
   # warnings about theory content and properties
   dir="$(dirname "$kf")/../../"
   if [ -e "$dir/$theory_header" ]; then
-    for function in check propagate ppStaticLearn notifyRestart presolve postsolve; do
+    for function in propagate ppStaticLearn notifyRestart presolve postsolve; do
        if eval "\$theory_has_$function"; then
          grep '\<'"$function"' *\((\|;\)' "$dir/$theory_header" | grep -vq '^ */\(/\|\*\)' ||
            echo "$kf: warning: $theory_class has property \"$function\" in its kinds file but doesn't appear to declare the function" >&2
-- 
2.30.2