summaryrefslogtreecommitdiff
path: root/src/theory/rewriterules/rr_trigger.h
diff options
context:
space:
mode:
authorlianah <lianahady@gmail.com>2013-03-13 13:44:33 -0400
committerlianah <lianahady@gmail.com>2013-03-13 13:44:33 -0400
commit3fcdb18fe92e5213aa708285c0d7d5e55633492b (patch)
treebbbd57efd9a8063a976a55afa7c384fb67db9b17 /src/theory/rewriterules/rr_trigger.h
parent267ad0ceb6808bd4c05d7c4bb04a7886efc19eab (diff)
parent9817df56827b4ee0ee67a33361f8619c5d1df6ed (diff)
post failed attempts at getting the incremental solver to work
Diffstat (limited to 'src/theory/rewriterules/rr_trigger.h')
-rw-r--r--src/theory/rewriterules/rr_trigger.h1
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;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback