Fix soundness bug for quantifier macros involving Int/Real.

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;