diff --git a/ir/memory.cpp b/ir/memory.cpp
index 77265ee26..0ea965064 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -1305,6 +1305,8 @@ void Memory::mkAxioms(const Memory &tgt) const {
   if (has_null_block)
     state->addAxiom(Pointer::mkNullPointer(*this).getAddress(false) == 0);
 
+  const unsigned max_quadratic_disjoint = 75;
+
   // Non-local blocks are disjoint.
   auto zero = expr::mkUInt(0, bits_ptr_address);
   auto one  = expr::mkUInt(1, bits_ptr_address);
@@ -1341,6 +1343,9 @@ void Memory::mkAxioms(const Memory &tgt) const {
           : addr.add_no_uoverflow(sz));
     }
 
+    if (num_nonlocals > max_quadratic_disjoint)
+      continue;
+
     // disjointness constraint
     for (unsigned bid2 = bid + 1; bid2 < num_nonlocals; ++bid2) {
       if (skip_bid(bid2))
@@ -1351,6 +1356,23 @@ void Memory::mkAxioms(const Memory &tgt) const {
                                p2.blockAlignment()));
     }
   }
+
+  // tame down quadratic explosion in disjointness constraint with a quantifier.
+  if (num_nonlocals > max_quadratic_disjoint) {
+    auto bid_ty = expr::mkUInt(0, Pointer::bitsShortBid());
+    expr bid1 = expr::mkFreshVar("#bid1", bid_ty);
+    expr bid2 = expr::mkFreshVar("#bid2", bid_ty);
+    expr offset = expr::mkUInt(0, bits_for_offset);
+    Pointer p1(*this, Pointer::mkLongBid(bid1, false), offset);
+    Pointer p2(*this, Pointer::mkLongBid(bid2, false), offset);
+    state->addAxiom(
+      expr::mkForAll({bid1, bid2},
+        bid1 == bid2 ||
+        disjoint(p1.getAddress(), p1.blockSize().zextOrTrunc(bits_ptr_address),
+                 p1.blockAlignment(),
+                 p2.getAddress(), p2.blockSize().zextOrTrunc(bits_ptr_address),
+                 p2.blockAlignment())));
+  }
 }
 
 void Memory::resetGlobals() {
diff --git a/llvm_util/cmd_args_def.h b/llvm_util/cmd_args_def.h
index 689cef515..0839aac5c 100644
--- a/llvm_util/cmd_args_def.h
+++ b/llvm_util/cmd_args_def.h
@@ -11,7 +11,7 @@ config::src_unroll_cnt = opt_unrolling_factor;
 config::disable_undef_input = opt_disable_undef;
 config::disable_poison_input = opt_disable_poison;
 config::tgt_is_asm = opt_tgt_is_asm;
-config::check_if_src_is_ub = opt_check_if_src_is_ub;
+config::fail_if_src_is_ub = opt_fail_if_src_is_ub;
 config::symexec_print_each_value = opt_se_verbose;
 smt::set_query_timeout(to_string(opt_smt_to));
 smt::set_memory_limit((uint64_t)opt_smt_max_mem * 1024 * 1024);
diff --git a/llvm_util/cmd_args_list.h b/llvm_util/cmd_args_list.h
index 7cf07b098..b732ec92a 100644
--- a/llvm_util/cmd_args_list.h
+++ b/llvm_util/cmd_args_list.h
@@ -40,9 +40,9 @@ llvm::cl::opt<bool> opt_disable_poison(LLVM_ARGS_PREFIX "disable-poison-input",
   llvm::cl::desc("Assume inputs are not poison (default=false)"),
   llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
 
-llvm::cl::opt<bool> opt_check_if_src_is_ub(
-  LLVM_ARGS_PREFIX "check-src-ub",
-  llvm::cl::desc("Check if source function is always UB (default=false)"),
+llvm::cl::opt<bool> opt_fail_if_src_is_ub(
+  LLVM_ARGS_PREFIX "fail-src-ub",
+  llvm::cl::desc("Fail if source function is always UB (default=false)"),
   llvm::cl::init(false), llvm::cl::cat(alive_cmdargs));
 
 llvm::cl::opt<bool> opt_tgt_is_asm(
diff --git a/llvm_util/compare.cpp b/llvm_util/compare.cpp
index 38803f47d..cb7bf2da6 100644
--- a/llvm_util/compare.cpp
+++ b/llvm_util/compare.cpp
@@ -108,6 +108,9 @@ bool Verifier::compareFunctions(llvm::Function &F1, llvm::Function &F2) {
     r.t.tgt.writeDot("tgt");
   }
 
+  if (r.errs.hasWarnings())
+    r.errs.printWarnings(out);
+
   switch (r.status) {
   case Results::ERROR:
     UNREACHABLE();
diff --git a/smt/ctx.cpp b/smt/ctx.cpp
index 0237ec6c1..5f18fb29c 100644
--- a/smt/ctx.cpp
+++ b/smt/ctx.cpp
@@ -31,6 +31,7 @@ void context::init() {
   Z3_global_param_set("model.partial", "true");
   Z3_global_param_set("smt.ematching", "false");
   Z3_global_param_set("smt.mbqi.max_iterations", "1000000");
+  Z3_global_param_set("smtlib2_compliant", "true");
   Z3_global_param_set("smt.random_seed", get_random_seed());
   Z3_global_param_set("timeout", get_query_timeout());
   Z3_global_param_set("memory_high_watermark", "2147483648"); // 2 GBs
diff --git a/tools/alive-tv.cpp b/tools/alive-tv.cpp
index 0e4962988..d97d673c8 100644
--- a/tools/alive-tv.cpp
+++ b/tools/alive-tv.cpp
@@ -145,7 +145,7 @@ and "tgt5" will unused.
       if (F1.isDeclaration())
         continue;
       auto SrcFName = F1.getName();
-      if (!SrcFName.startswith(opt_src_fn))
+      if (!SrcFName.starts_with(opt_src_fn))
         continue;
 
       // Check src{+d}/tgt{+d} variant
diff --git a/tools/alive.cpp b/tools/alive.cpp
index e21166420..1ca919f21 100644
--- a/tools/alive.cpp
+++ b/tools/alive.cpp
@@ -127,7 +127,9 @@ int main(int argc, char **argv) {
         bool correct = true;
         for (; types; ++types) {
           tv.fixupTypes(types);
-          if (auto errs = tv.verify()) {
+          auto errs = tv.verify();
+          errs.printWarnings(cerr);
+          if (errs) {
             cerr << errs;
             correct = false;
             break;
diff --git a/tools/transform.cpp b/tools/transform.cpp
index aba66aa20..57f47383f 100644
--- a/tools/transform.cpp
+++ b/tools/transform.cpp
@@ -502,10 +502,16 @@ check_refinement(Errors &errs, const Transform &t, State &src_state,
     axioms_expr = std::move(axioms)();
   }
 
-  if (config::check_if_src_is_ub &&
-      check_expr(axioms_expr && fndom_a).isUnsat()) {
-    errs.add("Source function is always UB", false);
-    return;
+  if (check_expr(axioms_expr && fndom_a).isUnsat()) {
+    if (config::fail_if_src_is_ub) {
+      errs.add("Source function is always UB", false);
+      return;
+    } else {
+      errs.addWarning(
+        "Source function is always UB.\n"
+        "It can be refined by any target function.\n"
+        "Please make sure this is what you wanted.");
+    }
   }
 
   {
diff --git a/tv/tv.cpp b/tv/tv.cpp
index 4ce4ab5c5..b9ecd1659 100644
--- a/tv/tv.cpp
+++ b/tv/tv.cpp
@@ -324,22 +324,28 @@ struct TVLegacyPass final : public llvm::ModulePass {
       assert(types.hasSingleTyping());
     }
 
-    if (Errors errs = verifier.verify()) {
-      *out << "Transformation doesn't verify!" <<
-              (errs.isUnsound() ? " (unsound)\n" : " (not unsound)\n")
-           << errs;
-      if (errs.isUnsound()) {
-        has_failure = true;
-        *out << "\nPass: " << pass_name << '\n';
-        emitCommandLine(out);
-        if (!SavedBitcode.empty())
-          writeBitcode(report_filename);
-        *out << "\n";
+    {
+      Errors errs = verifier.verify();
+      if (errs.hasWarnings())
+        errs.printWarnings(*out);
+
+      if (errs) {
+        *out << "Transformation doesn't verify!" <<
+                (errs.isUnsound() ? " (unsound)\n" : " (not unsound)\n")
+            << errs;
+        if (errs.isUnsound()) {
+          has_failure = true;
+          *out << "\nPass: " << pass_name << '\n';
+          emitCommandLine(out);
+          if (!SavedBitcode.empty())
+            writeBitcode(report_filename);
+          *out << "\n";
+        }
+        if (opt_error_fatal && has_failure)
+          finalize();
+      } else {
+        *out << "Transformation seems to be correct!\n\n";
       }
-      if (opt_error_fatal && has_failure)
-        finalize();
-    } else {
-      *out << "Transformation seems to be correct!\n\n";
     }
 
   done:
diff --git a/util/config.cpp b/util/config.cpp
index e5b40c027..82ab5f66a 100644
--- a/util/config.cpp
+++ b/util/config.cpp
@@ -16,7 +16,7 @@ string smt_benchmark_dir;
 bool disable_poison_input = false;
 bool disable_undef_input = false;
 bool tgt_is_asm = false;
-bool check_if_src_is_ub = false;
+bool fail_if_src_is_ub = false;
 bool disallow_ub_exploitation = false;
 bool debug = false;
 unsigned src_unroll_cnt = 0;
diff --git a/util/config.h b/util/config.h
index d4b694315..57f58c888 100644
--- a/util/config.h
+++ b/util/config.h
@@ -21,7 +21,7 @@ extern bool disable_undef_input;
 
 extern bool tgt_is_asm;
 
-extern bool check_if_src_is_ub;
+extern bool fail_if_src_is_ub;
 
 /// This is a special mode to verify that LLVM's optimizations are not
 /// exploiting UB. In particular, we disallow any UB related with arithmetic,
diff --git a/util/errors.cpp b/util/errors.cpp
index 4b8a79d6a..757b4cc18 100644
--- a/util/errors.cpp
+++ b/util/errors.cpp
@@ -33,6 +33,10 @@ void Errors::add(AliveException &&e) {
   add(std::move(e.msg), e.is_unsound);
 }
 
+void Errors::addWarning(const char *str) {
+  warnings.emplace(str);
+}
+
 bool Errors::isUnsound() const {
   for (auto &[msg, unsound] : errs) {
     if (unsound)
@@ -48,4 +52,12 @@ ostream& operator<<(ostream &os, const Errors &errs) {
   return os;
 }
 
+void Errors::printWarnings(std::ostream &os) const {
+  for (auto &str : warnings) {
+    os << "\n****************************************\n"
+          "WARNING: " << str
+       << "\n****************************************\n\n";
+  }
+}
+
 }
diff --git a/util/errors.h b/util/errors.h
index c53c75611..9c74ab9e0 100644
--- a/util/errors.h
+++ b/util/errors.h
@@ -22,6 +22,7 @@ struct AliveException {
 
 class Errors {
   std::set<std::pair<std::string, bool>> errs;
+  std::set<std::string> warnings;
 
 public:
   Errors() = default;
@@ -32,11 +33,14 @@ class Errors {
   void add(const char *str, bool is_unsound);
   void add(std::string &&str, bool is_unsound);
   void add(AliveException &&e);
+  void addWarning(const char *str);
 
   explicit operator bool() const { return !errs.empty(); }
   bool isUnsound() const;
+  bool hasWarnings() const { return !warnings.empty(); }
 
   friend std::ostream& operator<<(std::ostream &os, const Errors &e);
+  void printWarnings(std::ostream &os) const;
 };
 
 }