Minor fix for bounded integers.

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 6b53612d7e3c8b35d500eefc3f56eca101d3de67..3d5066c08cfc3b8d558431c34cf74a8391ce2af9 100644 (file)
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -797,6 +797,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
       Node l, u;
       getBoundValues( q, v, rsi, l, u );
       if( l.isNull() || u.isNull() ){
+        Trace("bound-int-warn") << "WARNING: Could not find integer bounds in model for " << v << " in " << q << std::endl;
         //failed, abort the iterator
         return false;
       }else{
@@ -824,6 +825,7 @@ bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node
     }else if( bvt==BOUND_SET_MEMBER  ){ 
       Node srv = getSetRangeValue( q, v, rsi );
       if( srv.isNull() ){
+        Trace("bound-int-warn") << "WARNING: Could not find set bound in model for " << v << " in " << q << std::endl;
         return false;
       }else{
         Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl;

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 88b5f5fb1dc9d8d0852082eef68db203137353ad..b1cc9ed197695a7f28ad37d3079e6e160ee31007 100644 (file)
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -70,6 +70,7 @@ Node FirstOrderModel::getAssertedQuantifier( unsigned i, bool ordered ) {
   }
 }
 
+//AJR : FIXME : this function is only used by bounded integers, can likely be removed.
 Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
   std::vector< Node > children;
   if( n.getNumChildren()>0 ){
@@ -92,7 +93,8 @@ Node FirstOrderModel::getCurrentModelValue( Node n, bool partial ) {
       return nn;
     }
   }else{
-    return getRepresentative(n);
+    //return getRepresentative(n);
+    return getValue(n);
   }
 }
 

diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index ec5255db704205bf500a6c5dd1250751da756543..be2a274b2df68d15982e01e1de5d14fc3f43d369 100644 (file)
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -68,7 +68,8 @@ TESTS =       \
        cons-sets-bounds.smt2 \
        bug651.smt2 \
        bug652.smt2 \
-       bug782.smt2
+       bug782.smt2 \
+       quant_real_univ.cvc
 
 EXTRA_DIST = $(TESTS)
 

diff --git a/test/regress/regress0/fmf/quant_real_univ.cvc b/test/regress/regress0/fmf/quant_real_univ.cvc
new file mode 100644 (file)
index 0000000..c3cefd7
--- /dev/null
+++ b/test/regress/regress0/fmf/quant_real_univ.cvc
@@ -0,0 +1,14 @@
+% EXPECT: sat\r
+OPTION "fmf-bound";\r
+Atom : TYPE;\r
+REAL_UNIVERSE : SET OF [REAL];\r
+ATOM_UNIVERSE : SET OF [Atom];\r
+ASSERT REAL_UNIVERSE = UNIVERSE :: SET OF [REAL];\r
+ASSERT ATOM_UNIVERSE = UNIVERSE :: SET OF [Atom];\r
+\r
+levelVal : SET OF [Atom, REAL];\r
+ASSERT FORALL (s : Atom, v1, v2 : REAL) : \r
+                       (TUPLE(s) IS_IN ATOM_UNIVERSE AND TUPLE(v1) IS_IN REAL_UNIVERSE AND TUPLE(v2) IS_IN REAL_UNIVERSE) \r
+                       => (((s, v1) IS_IN levelVal AND (s, v2) IS_IN levelVal) => (v1 = v2));\r
+\r
+CHECKSAT;                      \r