Fix bug 749.

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 7e896d358dbc646bcfb09464c5b14b5df17472ac..963889a85c45be38a87e1de0a6fa9eba11c6a3a2 100644 (file)
--- 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 a477b9f2fe4426c63f7c4e833d5074881914a9fe..6608ae22d5c791f794f01d134986323f8d6b7023 100644 (file)
--- 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 (file)
index 0000000..5fea8d4
--- /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)