diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-11 12:59:13 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-11-11 13:07:55 -0600 |
| commit | e2f28f39b3a3749a5eeed5294f25bec1e210b129 (patch) | |
| tree | 6bd5fc8c198139bdf518ad3ae443d87eac13816f /src/theory/quantifiers/trigger.cpp | |
| parent | 4ee85fbbe8f1bbc6261b804916f897b26d500fbf (diff) | |
Add simple inferences for extended bitvector functions, add a few related options. Use bv2nat, int2bv as triggers. Add regressions.
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
| -rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 3017238ca..7ab9f7065 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -354,7 +354,7 @@ bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || - k==SEP_PTO; + k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR; } bool Trigger::isRelationalTrigger( Node n ) { |