Add support for UBSan instrumentation (#3382)

This commit adds support for compiling CVC4 with UBSan instrumentation.
The commit also adds a dummy version of `AigBitblaster`. Previously,
when CVC4 was built without ABC, `AigBitblaster` was not fully defined
(the class was declared but the implementation was not being compiled).
This lead to missing RTTI information when compiling with UBSan
instrumentation.

1 files changed, 16 insertions, 0 deletions

diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h
index 8b63a9aa6..4e11c0f36 100644
--- a/src/theory/bv/bitblast/aig_bitblaster.h
+++ b/src/theory/bv/bitblast/aig_bitblaster.h
@@ -38,6 +38,8 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+#ifdef CVC4_USE_ABC
+
 class AigBitblaster : public TBitblaster<Abc_Obj_t*>
 {
  public:
@@ -108,7 +110,21 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*>
   Statistics d_statistics;
 };
 
+#else /* CVC4_USE_ABC */
+
+/**
+ * Dummy version of the AigBitblaster class that cannot be instantiated s.t. we
+ * can declare `std::unique_ptr<AigBitblaster>` without ABC.
+ */
+class AigBitblaster : public TBitblaster<Abc_Obj_t*>
+{
+  AigBitblaster() = delete;
+};
+
+#endif /* CVC4_USE_ABC */
+
 }  // namespace bv
 }  // namespace theory
 }  // namespace CVC4
+
 #endif  //  CVC4__THEORY__BV__BITBLAST__AIG_BITBLASTER_H