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

diff --git a/src/theory/bags/kinds b/src/theory/bags/kinds
index cd53484ebefabbd24ef2fa7d4c9860b6d06aceee..dd8eacfb5cc700aa873641aa982c6e87c68a4cb6 100644 (file)
--- 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 81e551a1054bcc2c15998893f136a030d29a2959..b2c6e1ef2bdd161d78f449f4a89c8004771c17d9 100755 (executable)
--- 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