From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Thu, 1 Apr 2021 16:18:27 +0000 (-0700)
Subject: kinds: Remove non-existent properties. (#6253)
X-Git-Tag: cvc5-1.0.0~1993
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=afaf4413775ff7d6054a5893f1397ad908e0773c;p=cvc5.git

kinds: Remove non-existent properties. (#6253)
---

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