diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
| commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
| tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/preprocessing/passes/quantifier_macros.cpp | |
| parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) | |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/preprocessing/passes/quantifier_macros.cpp')
| -rw-r--r-- | src/preprocessing/passes/quantifier_macros.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/preprocessing/passes/quantifier_macros.cpp b/src/preprocessing/passes/quantifier_macros.cpp index 0f71943c9..1d834ce60 100644 --- a/src/preprocessing/passes/quantifier_macros.cpp +++ b/src/preprocessing/passes/quantifier_macros.cpp @@ -199,7 +199,7 @@ bool QuantifierMacros::isGroundUfTerm( Node f, Node n ) { } bool QuantifierMacros::isBoundVarApplyUf( Node n ) { - Assert( n.getKind()==APPLY_UF ); + Assert(n.getKind() == APPLY_UF); TypeNode tno = n.getOperator().getType(); std::map< Node, bool > vars; // allow if a vector of unique variables of the same type as UF arguments @@ -437,7 +437,7 @@ Node QuantifierMacros::simplify( Node n ){ }else if( !etc.isConst() ){ cond.push_back( etc ); } - Assert( children[i].getType().isSubtypeOf( tno[i] ) ); + Assert(children[i].getType().isSubtypeOf(tno[i])); } if( success ){ //do substitution if necessary |