diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-20 16:02:14 -0500 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-09-20 16:02:22 -0500 |
| commit | 374fc2396a4f4338ade7ea0fb958e26c9e3bb982 (patch) | |
| tree | 841f9b1727ded2a82e15389c279e23e9ab024280 /src/theory/quantifiers/quant_conflict_find.cpp | |
| parent | e61e9853656d0a0d1c16cb095b9173dc2f732b21 (diff) | |
More refactoring of cbqi. Add a few regressions. Add option for qcf.
Diffstat (limited to 'src/theory/quantifiers/quant_conflict_find.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_conflict_find.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 522f4dfce..31831d73b 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -108,7 +108,7 @@ void QuantInfo::initialize( QuantConflictFind * p, Node q, Node qn ) { } Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; - if( d_mg->isValid() ){ + if( d_mg->isValid() && options::qcfEagerCheckRd() ){ //optimization : record variable argument positions for terms that must be matched std::vector< TNode > vars; //TODO: revisit this, makes QCF faster, but misses conflicts due to caring about paths that may not be relevant (starExec jobs 14136/14137) |