summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/quant_conflict_find.cpp
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-10-16 22:16:49 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2014-10-16 22:16:55 +0200
commit9d7378688486cb0dbad207482932dfb4b5d91f95 (patch)
tree11762aa3a877de82f3b578699c40ba37016efb79 /src/theory/quantifiers/quant_conflict_find.cpp
parent6d279143db69b153815165c752eae1432538ec2e (diff)
Make --user-pat=trust default. Fix a few warnings found by Morgan. Minor changes to options.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
-rwxr-xr-xsrc/theory/quantifiers/quant_conflict_find.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp
index 8136bf11e..f976a0dbf 100755
--- a/src/theory/quantifiers/quant_conflict_find.cpp
+++ b/src/theory/quantifiers/quant_conflict_find.cpp
@@ -1655,7 +1655,7 @@ bool MatchGen::isHandledBoolConnective( TNode n ) {
bool MatchGen::isHandledUfTerm( TNode n ) {
//return n.getKind()==APPLY_UF || n.getKind()==STORE || n.getKind()==SELECT ||
// n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR_TOTAL || n.getKind()==APPLY_TESTER;
- return inst::Trigger::isAtomicTriggerKind( n.getKind() );
+ return inst::Trigger::isAtomicTriggerKind( n.getKind() );
}
Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
@@ -1683,7 +1683,6 @@ bool MatchGen::isHandled( TNode n ) {
QuantConflictFind::QuantConflictFind( QuantifiersEngine * qe, context::Context* c ) :
QuantifiersModule( qe ),
-d_c( c ),
d_conflict( c, false ),
d_qassert( c ) {
d_fid_count = 0;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback