Preliminary version of finite model finding over bounded integer quantification. Minor update to casc script.

1 files changed, 7 insertions, 1 deletions

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 6b07a87e0..53f67853b 100644
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -71,7 +71,7 @@ bool QuantArith::isolate( Node v, std::map< Node, Node >& msum, Node & veq, Kind
     Rational r = msum[v].isNull() ? Rational(1) : msum[v].getConst<Rational>();
     if ( r.sgn()!=0 ){
       for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
-        if( it->first!=v ){
+        if( it->first.isNull() || it->first!=v ){
           Node m;
           if( !it->first.isNull() ){
             if ( !it->second.isNull() ){
@@ -111,6 +111,12 @@ Node QuantArith::negate( Node t ) {
   return tt;
 }
 
+Node QuantArith::offset( Node t, int i ) {
+  Node tt = NodeManager::currentNM()->mkNode( PLUS, NodeManager::currentNM()->mkConst( Rational(i) ), t );
+  tt = Rewriter::rewrite( tt );
+  return tt;
+}
+
 
 void QuantRelevance::registerQuantifier( Node f ){
   //compute symbols in f