From: Morgan Deters <mdeters@gmail.com>
Date: Mon, 14 May 2012 19:10:39 +0000 (+0000)
Subject: in debug builds, -d can be used for trace tags that aren't also debug tags
X-Git-Tag: cvc5-1.0.0~8182
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=39ec0e8bb0ada53e9e47cee025df1dad003746c0;p=cvc5.git

in debug builds, -d can be used for trace tags that aren't also debug tags
---

diff --git a/src/util/options.cpp b/src/util/options.cpp
index a9405fb25..36033db0b 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -577,7 +577,7 @@ throw(OptionException) {
 
     case 'd':
       if(Configuration::isDebugBuild() && Configuration::isTracingBuild()) {
-        if(!Configuration::isDebugTag(optarg)) {
+        if(!Configuration::isDebugTag(optarg) && !Configuration::isTraceTag(optarg)) {
           throw OptionException(string("debug tag ") + optarg +
                                 string(" not available"));
         }