diff options
| author | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-02-13 23:12:04 -0600 |
|---|---|---|
| committer | Tianyi Liang <tianyi-liang@uiowa.edu> | 2013-02-13 23:12:04 -0600 |
| commit | c33a1abc78bcd51f3f95562b117498caf252cafc (patch) | |
| tree | 51528bcb774091e02fede9f268fb2eb904fc7e16 | |
| parent | e9d8ae34db4c4a8161cc1abdfb225c3e9e2bd9ee (diff) | |
repairs a bug in rewriterule engine: constructor cannot be used as a pattern
| -rw-r--r-- | src/theory/rewriterules/rr_trigger.h | 1 |
1 files changed, 1 insertions, 0 deletions
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; } |