diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-17 17:35:41 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-17 17:35:41 +0200 |
commit | 944961607aa4a16c97d32e605c3f609ab66b4dc5 (patch) | |
tree | 33c85f76ae63081b80a4ba1c38250bc5618f3cf0 /src/theory | |
parent | 83f4a3a884f53fa02019d1dab308240f0027c908 (diff) |
Fix soundness bug for quantifier macros involving Int/Real.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/macros.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 11734c43f..7321e22b4 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -98,10 +98,14 @@ bool QuantifierMacros::isMacroLiteral( Node n, bool pol ){ bool QuantifierMacros::isBoundVarApplyUf( Node n ) { Assert( n.getKind()==APPLY_UF ); + TypeNode tn = n.getOperator().getType(); for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( n[i].getKind()!=BOUND_VARIABLE ){ return false; } + if( n[i].getType()!=tn[i] ){ + return false; + } for( unsigned j=0; j<i; j++ ){ if( n[j]==n[i] ){ return false; |