From a362e943bf543b7bd31d14525f8f76e15cb65f87 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Thu, 1 Aug 2019 09:36:10 -0700
Subject: Bidirectional quantifier instantiation

---
 src/theory/quantifiers/fmf/bounded_integers.cpp | 15 +++++++++++----
 1 file changed, 11 insertions(+), 4 deletions(-)

diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp
index f873b94f2..ac5566405 100644
--- a/src/theory/quantifiers/fmf/bounded_integers.cpp
+++ b/src/theory/quantifiers/fmf/bounded_integers.cpp
@@ -746,10 +746,17 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
         if( ra==d_quantEngine->getTermUtil()->d_true ){
           long rr = range.getConst<Rational>().getNumerator().getLong()+1;
           Trace("bound-int-rsi")  << "Actual bound range is " << rr << std::endl;
-          for( unsigned k=0; k<rr; k++ ){
-            Node t = NodeManager::currentNM()->mkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) );
-            t = Rewriter::rewrite( t );
-            elements.push_back( t );
+          for (unsigned k = 0; k < rr; k++)
+          {
+            Node t = NodeManager::currentNM()->mkNode(
+                PLUS, tl, NodeManager::currentNM()->mkConst(Rational(k)));
+            t = Rewriter::rewrite(t);
+            elements.push_back(t);
+
+            Node t2 = NodeManager::currentNM()->mkNode(
+                MINUS, tu, NodeManager::currentNM()->mkConst(Rational(k)));
+            t2 = Rewriter::rewrite(t2);
+            elements.push_back(t2);
           }
           return true;
         }else{
-- 
cgit v1.2.3