diff options
-rw-r--r-- | src/theory/bags/kinds | 4 | ||||
-rwxr-xr-x | 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 |