From: Tim King <taking@cs.nyu.edu>
Date: Tue, 31 Oct 2017 21:39:45 +0000 (-0700)
Subject: CID 1459592: Always checking whether rd is null or not. (#1299)
X-Git-Tag: cvc5-1.0.0~5520
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b6551c529506592da7c66e39a911d9299944eb8;p=cvc5.git

CID 1459592: Always checking whether rd is null or not. (#1299)
---

diff --git a/src/theory/quantifiers/inst_strategy_enumerative.cpp b/src/theory/quantifiers/inst_strategy_enumerative.cpp
index 8b825d50d..67930ce2b 100644
--- a/src/theory/quantifiers/inst_strategy_enumerative.cpp
+++ b/src/theory/quantifiers/inst_strategy_enumerative.cpp
@@ -135,7 +135,7 @@ bool InstStrategyEnum::process(Node f, bool fullEffort)
         Trace("inst-alg") << "-> Ground term instantiate " << f << "..."
                           << std::endl;
       }
-      Assert(rd != NULL);
+      AlwaysAssert(rd);
       Trace("inst-alg-debug") << "Compute relevant domain..." << std::endl;
       rd->compute();
       Trace("inst-alg-debug") << "...finished" << std::endl;