Enable IC3SA for arrays (stanford-centaur#332)

Array sorts work with the current IC3SA infrastructure. They occupy their own equivalence classes separate from bit-vectors.
CyanoKobalamyne · Jul 10, 2024 · b82d87e · b82d87e
1 parent 36f0e81
commit b82d87e
Showing 1 changed file with 3 additions and 3 deletions.
diff --git a/engines/ic3sa.cpp b/engines/ic3sa.cpp
@@ -199,9 +199,9 @@ void IC3SA::check_ts() const
 
   for (const auto & sv : ts_.statevars()) {
     SortKind sk = sv->get_sort()->get_sort_kind();
-    if (sk != BOOL && sk != BV)
-    {
-      throw PonoException("IC3SA currently only supports bit-vectors");
+    if (sk != BOOL && sk != BV && sk != ARRAY) {
+      throw PonoException(
+          "IC3SA currently only supports bit-vectors and arrays");
     }
   }
 }