diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 17:38:53 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-07 17:38:59 +0100 |
| commit | 4ad0191e20e4d812d9a5dc3a733153cb10f6d728 (patch) | |
| tree | f25fa219a0d464ca7a30b40d27fa45b05ff33638 /src/theory/quantifiers_engine.cpp | |
| parent | 3a3a57583fd8bd4af5c3b99b0047c9b20de38bb1 (diff) | |
Enable --quant-cf by default. Fix bug in qcf for mixed Int/Real. Minor improvement to performance of E-matching.
Diffstat (limited to 'src/theory/quantifiers_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers_engine.cpp | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 46995653f..eabba85bf 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -524,6 +524,7 @@ bool QuantifiersEngine::addInstantiation( Node f, std::vector< Node >& vars, std for( int i=0; i<(int)terms.size(); i++ ){ Trace("inst") << " " << terms[i]; Trace("inst") << std::endl; + Assert( terms[i].getType().isSubtypeOf( f[0][i].getType() ) ); } if( options::cbqi() ){ for( int i=0; i<(int)terms.size(); i++ ){ |