diff options
Diffstat (limited to 'src/theory/sort_inference.cpp')
| -rw-r--r-- | src/theory/sort_inference.cpp | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 83062ce48..d44492259 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -405,10 +405,10 @@ int SortInference::process( Node n, std::map< Node, Node >& var_bound, std::map< for( size_t i=0; i<n.getNumChildren(); i++ ){ bool processChild = true; if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ - processChild = - options::userPatternsQuant() == options::UserPatMode::IGNORE - ? i == 1 - : i >= 1; + processChild = options().quantifiers.userPatternsQuant + == options::UserPatMode::IGNORE + ? i == 1 + : i >= 1; } if( processChild ){ children.push_back( n[i] ); @@ -672,10 +672,10 @@ Node SortInference::simplifyNode( for( size_t i=0; i<n.getNumChildren(); i++ ){ bool processChild = true; if( n.getKind()==kind::FORALL || n.getKind()==kind::EXISTS ){ - processChild = - options::userPatternsQuant() == options::UserPatMode::IGNORE - ? i == 1 - : i >= 1; + processChild = options().quantifiers.userPatternsQuant + == options::UserPatMode::IGNORE + ? i == 1 + : i >= 1; } if( processChild ){ if (isHandledApplyUf(n.getKind())) |