repairs a bug in rewriterule engine: constructor cannot be used as a pattern

diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h
index 7be5d15079b1fc5c09a40fefc494238ed219d62a..f11d6ed664935cf2c88418c11a034abfe6332596 100644 (file)
--- a/src/theory/rewriterules/rr_trigger.h
+++ b/src/theory/rewriterules/rr_trigger.h
@@ -100,6 +100,7 @@ public:
   static inline bool isAtomicTrigger( TNode n ){
     return
       n.getKind()==kind::APPLY_UF ||
+      n.getKind() == kind::APPLY_CONSTRUCTOR ||
       n.getKind()==kind::SELECT ||
       n.getKind()==kind::STORE;
   }