minor

HanielB · Feb 16, 2024 · 9ddf727 · 9ddf727
1 parent 17e9da1
commit 9ddf727
Showing 1 changed file with 18 additions and 1 deletion.
diff --git a/src/proof/alethe/alethe_node_converter.cpp b/src/proof/alethe/alethe_node_converter.cpp
@@ -107,8 +107,25 @@ Node AletheNodeConverter::postConvert(Node n)
           Trace("alethe-conv") << ".. witness: " << witness << "\n";
           return convert(witness);
         }
+        Unreachable() << "Could not convert Skolemization result from " << cacheVal << "\n";
       }
-      Unreachable() << "Fresh Skolem " << sfi << " is not allowed\n";
+      if (sfi == SkolemFunId::ARRAY_DEQ_DIFF)
+      {
+        Node v = nm->mkBoundVar(n.getType());
+        // the cache for this skolem must be an sexpr with the two arrays
+        Node def =
+            nm->mkNode(Kind::IMPLIES,
+                       cacheVal[0].eqNode(cacheVal[1]).notNode(),
+                       nm->mkNode(Kind::SELECT, cacheVal[0], v)
+                           .eqNode(nm->mkNode(Kind::SELECT, cacheVal[1], v))
+                           .notNode());
+        wi =
+            nm->mkNode(Kind::WITNESS, nm->mkNode(Kind::BOUND_VAR_LIST, v), def);
+        Trace("alethe-conv") << "Built " << wi << "\n";
+        return convert(wi);
+      }
+      Unreachable() << "Fresh Skolem [" << sfi << "] " << n
+                    << " is not supported in Alethe\n";
     }
     case Kind::FORALL:
     {