From: Tianyi Liang <tianyi-liang@uiowa.edu>
Date: Thu, 14 Feb 2013 05:12:04 +0000 (-0600)
Subject: repairs a bug in rewriterule engine: constructor cannot be used as a pattern
X-Git-Tag: cvc5-1.0.0~7406^2~6
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1848dd58c980e49cd0ebe54ff39891e64da752d4;p=cvc5.git

repairs a bug in rewriterule engine: constructor cannot be used as a pattern
(cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc)

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
---

diff --git a/src/theory/rewriterules/rr_trigger.h b/src/theory/rewriterules/rr_trigger.h
index 7be5d1507..f11d6ed66 100644
--- 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;
   }