diff options
Diffstat (limited to 'src/theory/quantifiers/fun_def_process.cpp')
| -rw-r--r-- | src/theory/quantifiers/fun_def_process.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/theory/quantifiers/fun_def_process.cpp b/src/theory/quantifiers/fun_def_process.cpp index 185a349c0..aa3efca19 100644 --- a/src/theory/quantifiers/fun_def_process.cpp +++ b/src/theory/quantifiers/fun_def_process.cpp @@ -36,7 +36,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { for( unsigned i=0; i<assertions.size(); i++ ){ Node n = QuantAttributes::getFunDefHead( assertions[i] ); if( !n.isNull() ){ - Assert( n.getKind()==APPLY_UF ); + Assert(n.getKind() == APPLY_UF); Node f = n.getOperator(); //check if already defined, if so, throw error @@ -127,7 +127,7 @@ void FunDefFmf::simplify( std::vector< Node >& assertions ) { Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Node >& constraints, Node hd, bool is_fun_def, std::map< int, std::map< Node, Node > >& visited, std::map< int, std::map< Node, Node > >& visited_cons ) { - Assert( constraints.empty() ); + Assert(constraints.empty()); int index = ( is_fun_def ? 1 : 0 ) + 2*( hasPol ? ( pol ? 1 : -1 ) : 0 ); std::map< Node, Node >::iterator itv = visited[index].find( n ); if( itv!=visited[index].end() ){ @@ -240,7 +240,7 @@ Node FunDefFmf::simplifyFormula( Node n, bool pol, bool hasPol, std::vector< Nod cons = constraints[0]; } visited_cons[index][n] = cons; - Assert( constraints.size()==1 && constraints[0]==cons ); + Assert(constraints.size() == 1 && constraints[0] == cons); } visited[index][n] = ret; return ret; |