From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Wed, 17 Sep 2014 15:35:41 +0000 (+0200)
Subject: Fix soundness bug for quantifier macros involving Int/Real.
X-Git-Tag: cvc5-1.0.0~6629
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=944961607aa4a16c97d32e605c3f609ab66b4dc5;p=cvc5.git

Fix soundness bug for quantifier macros involving Int/Real.
---

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;
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 7e8e1ea99..41f66f92f 100644
--- 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
index 000000000..d29ddfe8f
--- /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