1. Fix for inst_match.cpp to allow compilation on fedora

2. Initial implementation of computeIsConst for arrays - still needs
   additional checks based on cardinality
3. Finally fixed pre-competition bug in array rewriter
4. Still to come: array rewrites for constants and STORE_ALL

1 files changed, 5 insertions, 1 deletions

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 271e04968..14a84ea72 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -31,8 +31,10 @@ using namespace CVC4;
 using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
-using namespace CVC4::theory::inst;
 
+namespace CVC4 {
+namespace theory {
+namespace inst {
 
 InstMatch::InstMatch() {
 }
@@ -878,3 +880,5 @@ int InstMatchGeneratorSimple::addTerm( Node f, Node t, QuantifiersEngine* qe ){
   }
   return qe->addInstantiation( f, m ) ? 1 : 0;
 }
+
+}}}