summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/bounded_integers.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-09-13 11:23:30 -0500
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2013-09-15 13:43:31 -0500
commit5aa5b7588230a4e61abb3a7bda132120618a3efa (patch)
treeb0c3556247cf3777cfa0352da3aa15f858e57458 /src/theory/quantifiers/bounded_integers.cpp
parentc46f66e6e50506f5e9c10df3dcb6db5affc45c78 (diff)
Change default option of simple ite lifting within quantifier bodies. add some debug messages.
Diffstat (limited to 'src/theory/quantifiers/bounded_integers.cpp')
-rw-r--r--src/theory/quantifiers/bounded_integers.cpp2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index 13e075265..e1e2f96c2 100644
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -290,6 +290,8 @@ void BoundedIntegers::registerQuantifier( Node f ) {
}
}
}
+ }else{
+ Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl;
}
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback