summaryrefslogtreecommitdiff
path: root/src/preprocessing
diff options
context:
space:
mode:
authorGereon Kremer <nafur42@gmail.com>2021-11-04 18:16:12 -0700
committerGitHub <noreply@github.com>2021-11-05 01:16:12 +0000
commit4669bb1ab2fce322cd8e3e172e57f0aa3006e1d7 (patch)
treea96dbf6ee19c1be29b24a2b92fd38dad9553a443 /src/preprocessing
parent6d947b4f85d005681ff438c6bd8ef7bba557be10 (diff)
Eliminate `Warning` macro in favor of `EnvObj::warning` (#7575)
This PR eliminates almost all usages of the Warning macro, replacing it mostly by calling EnvObj::warning.
Diffstat (limited to 'src/preprocessing')
-rw-r--r--src/preprocessing/passes/miplib_trick.cpp4
-rw-r--r--src/preprocessing/passes/sep_skolem_emp.cpp2
2 files changed, 1 insertions, 5 deletions
diff --git a/src/preprocessing/passes/miplib_trick.cpp b/src/preprocessing/passes/miplib_trick.cpp
index 61be4395b..59f046262 100644
--- a/src/preprocessing/passes/miplib_trick.cpp
+++ b/src/preprocessing/passes/miplib_trick.cpp
@@ -586,10 +586,6 @@ PreprocessingPassResult MipLibTrick::applyInternal(
Node newAssertion = var.eqNode(rewrite(sum));
if (top_level_substs.hasSubstitution(newAssertion[0]))
{
- // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl;
- // Warning() << "REPLACE " << newAssertion[1] << endl;
- // Warning() << "ORIG " <<
- // top_level_substs.getSubstitution(newAssertion[0]) << endl;
Assert(top_level_substs.getSubstitution(newAssertion[0])
== newAssertion[1]);
}
diff --git a/src/preprocessing/passes/sep_skolem_emp.cpp b/src/preprocessing/passes/sep_skolem_emp.cpp
index dd85bec69..5d3a1112e 100644
--- a/src/preprocessing/passes/sep_skolem_emp.cpp
+++ b/src/preprocessing/passes/sep_skolem_emp.cpp
@@ -111,7 +111,7 @@ PreprocessingPassResult SepSkolemEmp::applyInternal(
TypeNode locType, dataType;
if (!d_preprocContext->getTheoryEngine()->getSepHeapTypes(locType, dataType))
{
- Warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
+ warning() << "SepSkolemEmp::applyInternal: failed to get separation logic "
"heap types during preprocessing"
<< std::endl;
return PreprocessingPassResult::NO_CONFLICT;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback