From 9b32405be875e7d20289d8eabbe85d036a31f301 Mon Sep 17 00:00:00 2001
From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 15 Jun 2015 10:59:23 +0200
Subject: Make array basis term a skolem (avoids crashing in fmf).

---
 src/theory/quantifiers/term_database.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 2507209f4..eba080a0e 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -571,7 +571,7 @@ Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
     Node mbt;
     if( tn.isInteger() || tn.isReal() ){
       mbt = NodeManager::currentNM()->mkConst( Rational( 0 ) );
-    }else if( !tn.isSort() ){
+    }else if( !tn.isArray() && !tn.isSort() ){
       mbt = tn.mkGroundTerm();
     }else{
       if( options::fmfFreshDistConst() || d_type_map[ tn ].empty() ){
-- 
cgit v1.2.3