From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Thu, 28 Jul 2016 16:21:59 +0000 (-0500)
Subject: Fix bug 749.
X-Git-Tag: cvc5-1.0.0~6040^2~17^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4b0f7836db3bb6a2a0e912aeae1cd87f1823cfa8;p=cvc5.git

Fix bug 749.
---

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 7e896d358..963889a85 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -957,20 +957,27 @@ bool QuantifiersRewriter::computeVariableElimLit( Node lit, bool pol, std::vecto
               Node veq_c;
               Node val;
               int ires = QuantArith::isolate( itm->first, msum, veq_c, val, lit.getKind() );
-              if( ires!=0 && veq_c.isNull() && isVariableElim( itm->first, val ) ){
+              if( ires!=0 && veq_c.isNull() ){
                 bool is_upper = pol!=( ires==1 );
                 Trace("var-elim-ineq-debug") << lit << " is a " << ( is_upper ? "upper" : "lower" ) << " bound for " << itm->first << std::endl;
                 Trace("var-elim-ineq-debug") << "  pol/ires = " << pol << " " << ires << std::endl;
                 num_bounds[itm->first][is_upper][lit] = pol;
+              }else{
+                Trace("var-elim-ineq-debug") << "...ineligible " << itm->first << " since it cannot be solved for (" << ires << ", " << veq_c << ")." << std::endl;
+                num_bounds[itm->first][true].clear();
+                num_bounds[itm->first][false].clear();
               }
             }
           }else{
-            //compute variables in itm->first, these are not eligible for elimination
-            std::vector< Node > bvs;
-            TermDb::getBoundVars( itm->first, bvs );
-            for( unsigned j=0; j<bvs.size(); j++ ){
-              num_bounds[bvs[j]][true].clear();
-              num_bounds[bvs[j]][false].clear();
+            if( lit.getKind()==GEQ || lit.getKind()==GT ){
+              //compute variables in itm->first, these are not eligible for elimination
+              std::vector< Node > bvs;
+              TermDb::getBoundVars( itm->first, bvs );
+              for( unsigned j=0; j<bvs.size(); j++ ){
+                Trace("var-elim-ineq-debug") << "...ineligible " << bvs[j] << " since it is contained in monomial." << std::endl;
+                num_bounds[bvs[j]][true].clear();
+                num_bounds[bvs[j]][false].clear();
+              }
             }
           }
         }
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index a477b9f2f..6608ae22d 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -85,7 +85,8 @@ TESTS =	\
 	small-bug1-fixpoint-3.smt2 \
 	z3.620661-no-fv-trigger.smt2 \
 	bug_743.smt2 \
-	quaternion_ds1_symm_0428.fof.smt2
+	quaternion_ds1_symm_0428.fof.smt2 \
+	bug749-rounding.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/bug749-rounding.smt2 b/test/regress/regress0/quantifiers/bug749-rounding.smt2
new file mode 100644
index 000000000..5fea8d4ff
--- /dev/null
+++ b/test/regress/regress0/quantifiers/bug749-rounding.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --var-ineq-elim-quant
+; EXPECT: unknown
+(set-logic UFLIRA)
+
+(declare-fun round2 (Real) Int)
+
+(assert (forall ((x Real) (i Int)) (=> (<= x (to_real i)) (<= (round2 x) i)) ))
+(assert (forall ((x Real) (i Int)) (=> (<= (to_real i) x) (<= i (round2 x))) ))
+
+
+(check-sat)