diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-07 11:37:24 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-07 11:37:32 +0200 |
| commit | 1e7207dc661a1aa7d6509cc21d86fb757938efb1 (patch) | |
| tree | a1656d3a0c884bb03bc29ad4aff98a8dad1a9608 /src/theory/quantifiers/instantiation_engine.cpp | |
| parent | 26b9453941c0c90b887839246882be3629439ccf (diff) | |
Minor fixes for cegqi.
Diffstat (limited to 'src/theory/quantifiers/instantiation_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/instantiation_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index cb01fd373..ea3e18be1 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -328,7 +328,7 @@ bool InstantiationEngine::hasNonArithmeticVariable( Node f ){ } bool InstantiationEngine::doCbqi( Node f ){ - if( options::cbqi.wasSetByUser() ){ + if( options::cbqi.wasSetByUser() || options::cbqi2.wasSetByUser() ){ return options::cbqi(); }else if( options::cbqi() ){ //if quantifier has a non-arithmetic variable, then do not use cbqi |