Fix soundness bug for quantifier macros involving Int/Real.

diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp
index 11734c43f1c5f6304f162d3f5e076d1c9140fdb9..7321e22b4ab8d427b662118e1f540a2b5ab8e3b5 100644 (file)
--- 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;

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 7e8e1ea9921e31399c9f1d59344222c10c1c7b9e..41f66f92fc7e38bc3075741c8782fc753ec052c6 100644 (file)
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -43,7 +43,8 @@ TESTS =       \
        javafe.ast.StmtVec.009.smt2 \
        ARI176e1.smt2 \
         bi-artm-s.smt2 \
-       simp-typ-test.smt2
+       simp-typ-test.smt2 \
+       macros-int-real.smt2
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2

diff --git a/test/regress/regress0/quantifiers/macros-int-real.smt2 b/test/regress/regress0/quantifiers/macros-int-real.smt2
new file mode 100644 (file)
index 0000000..d29ddfe
--- /dev/null
+++ b/test/regress/regress0/quantifiers/macros-int-real.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --macros-quant
+; EXPECT: unknown
+(set-logic AUFLIRA)
+
+(declare-fun round2 (Real) Int)
+(assert (forall ((i Int))  (= (round2 (to_real i)) i)))
+
+(assert (= (round2 1.5) 1))
+(check-sat)
\ No newline at end of file