Do not eliminate non-standard arithmetic operators in recursive function definitions, add regression.

4 files changed, 29 insertions, 9 deletions

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 2b7e19c48..01352217e 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -510,16 +510,17 @@ Node QuantifiersRewriter::computeProcessTerms( Node body, std::vector< Node >& n
     Node fbody = TermDb::getFunDefBody( q );
     Assert( !body.isNull() );
     Trace("quantifiers-rewrite-debug") << "Decompose " << h << " / " << fbody << " as function definition for " << q << "." << std::endl;
-    Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds );
+    Node r = computeProcessTerms2( fbody, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, false );
+    Assert( new_vars.size()==h.getNumChildren() );
     return Rewriter::rewrite( NodeManager::currentNM()->mkNode( EQUAL, h, r ) );
   }else{
-    return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds );
+    return computeProcessTerms2( body, true, true, curr_cond, 0, cache, icache, new_vars, new_conds, options::elimExtArithQuant() );
   }
 }
 
 Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                                 std::map< Node, Node >& cache, std::map< Node, Node >& icache,
-                                                std::vector< Node >& new_vars, std::vector< Node >& new_conds ) {
+                                                std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith ) {
   Trace("quantifiers-rewrite-term-debug2") << "computeProcessTerms " << body << " " << hasPol << " " << pol << std::endl;
   Node ret;
   std::map< Node, Node >::iterator iti = cache.find( body );
@@ -593,14 +594,14 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
           bool newHasPol;
           bool newPol;
           QuantPhaseReq::getPolarity( body, i, hasPol, pol, newHasPol, newPol );
-          Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+          Node nn = computeProcessTerms2( body[i], newHasPol, newPol, currCond, nCurrCond, cache, icache, new_vars, new_conds, elimExtArith );
           if( body.getKind()==ITE && i==0 ){
             int res = getEntailedCond( nn, currCond );
             Trace("quantifiers-rewrite-term-debug") << "Condition for " << body << " is " << nn << ", entailment check=" << res << std::endl;
             if( res==1 ){
-              ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+              ret = computeProcessTerms2( body[1], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds, elimExtArith );
             }else if( res==-1 ){
-              ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds );
+              ret = computeProcessTerms2( body[2], hasPol, pol, currCond, nCurrCond, cache, icache, new_vars, new_conds, elimExtArith );
             }
           }
           children.push_back( nn );
@@ -681,7 +682,7 @@ Node QuantifiersRewriter::computeProcessTerms2( Node body, bool hasPol, bool pol
         ret = ite_v;
       }
       */
-    }else if( options::elimExtArithQuant() ){
+    }else if( elimExtArith ){
       if( ret.getKind()==INTS_DIVISION_TOTAL || ret.getKind()==INTS_MODULUS_TOTAL ){
         Node num = ret[0];
         Node den = ret[1];
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 90a22f4b7..c61ca1fb0 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -43,7 +43,7 @@ private:
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
   static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond,
                                     std::map< Node, Node >& cache, std::map< Node, Node >& icache,
-                                    std::vector< Node >& new_vars, std::vector< Node >& new_conds );
+                                    std::vector< Node >& new_vars, std::vector< Node >& new_conds, bool elimExtArith );
   static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj );
   static bool isConditionalVariableElim( Node n, int pol=0 );
   static bool isVariableElim( Node v, Node s );
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index a91499a6c..593cdfa8b 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -72,7 +72,8 @@ TESTS =	\
 	quant_real_univ.cvc \
 	constr-ground-to.smt2 \
 	bug-041417-set-options.cvc \
-	alg202+1.smt2
+	alg202+1.smt2 \
+	fmf-fun-no-elim-ext-arith.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2 b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
new file mode 100644
index 000000000..dd9cb6886
--- /dev/null
+++ b/test/regress/regress0/fmf/fmf-fun-no-elim-ext-arith.smt2
@@ -0,0 +1,18 @@
+; COMMAND-LINE: --fmf-fun --no-check-models
+; EXPECT: sat
+(set-logic UFLIA)
+(set-info :status sat)
+(define-fun-rec int-and ((n Int) (n1 Int) (n2 Int)) Bool (
+    or
+    (= n1 n 0)
+    (= n2 n 0)
+    (
+        and
+        (> n1 0)
+        (> n2 0)
+        (>= n 0)
+        (= (not (= (mod n 2 ) 0)) (and (not (= (mod n1 2 ) 0)) (not (= (mod n2 2) 0))))
+        (int-and (div n 2) (div n1 2) (div n2 2))
+    )
+))
+(check-sat)