From 1848dd58c980e49cd0ebe54ff39891e64da752d4 Mon Sep 17 00:00:00 2001 From: Tianyi Liang Date: Wed, 13 Feb 2013 23:12:04 -0600 Subject: [PATCH] repairs a bug in rewriterule engine: constructor cannot be used as a pattern (cherry picked from commit c33a1abc78bcd51f3f95562b117498caf252cafc) Signed-off-by: Morgan Deters --- src/theory/rewriterules/rr_trigger.h | 1 + 1 file changed, 1 insertion(+) 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; } -- 2.30.2