From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 15 Jun 2015 08:59:23 +0000 (+0200)
Subject: Make array basis term a skolem (avoids crashing in fmf).
X-Git-Tag: cvc5-1.0.0~6271
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b32405be875e7d20289d8eabbe85d036a31f301;p=cvc5.git

Make array basis term a skolem (avoids crashing in fmf).
---

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() ){