* disallow internal uses of mkVar() (you have to mkSkolem())

* add support for mkBoundVar() (BOUND_VAR_LISTs in quantifiers must be bound vars)

2 files changed, 2 insertions, 2 deletions

diff --git a/src/theory/arrays/theory_arrays.cpp b/src/theory/arrays/theory_arrays.cpp
index 4f2497d2b..4beab2d61 100644
--- a/src/theory/arrays/theory_arrays.cpp
+++ b/src/theory/arrays/theory_arrays.cpp
@@ -694,7 +694,7 @@ void TheoryArrays::check(Effort e) {
             TNode k;
             std::hash_map<TNode, Node, TNodeHashFunction>::iterator it = d_diseqCache.find(fact);
             if (it == d_diseqCache.end()) {
-              Node newk = nm->mkVar(indexType);
+              Node newk = nm->mkSkolem(indexType);
 	      Dump.declareVar(newk.toExpr(),
                               "an extensional lemma index variable from the theory of arrays");
               d_diseqCache[fact] = newk;
diff --git a/src/theory/arrays/theory_arrays_model.cpp b/src/theory/arrays/theory_arrays_model.cpp
index 7a574fac1..5c969060d 100644
--- a/src/theory/arrays/theory_arrays_model.cpp
+++ b/src/theory/arrays/theory_arrays_model.cpp
@@ -29,7 +29,7 @@ using namespace CVC4::theory::arrays;
 ArrayModel::ArrayModel( Node arr, quantifiers::FirstOrderModel* m ) : d_model( m ), d_arr( arr ){
   Assert( arr.getKind()!=STORE );
   //look at ground assertions
-  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkVar( arr.getType().getArrayIndexType() ) );
+  Node sel = NodeManager::currentNM()->mkNode( SELECT, arr, NodeManager::currentNM()->mkSkolem( arr.getType().getArrayIndexType() ) );
   Node sel_op = sel.getOperator();  //FIXME: easier way to do this?
   for( size_t i=0; i<d_model->getTermDatabase()->d_op_map[ sel_op ].size(); i++ ){
     Node n = d_model->getTermDatabase()->d_op_map[ sel_op ][i];