summaryrefslogtreecommitdiff
path: root/src/theory/model.cpp
diff options
context:
space:
mode:
authorAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-10-03 23:04:08 +0000
committerAndrew Reynolds <andrew.j.reynolds@gmail.com>2012-10-03 23:04:08 +0000
commit5c4debb1893109a4d4a2feacd910d3778aeca8f4 (patch)
tree306d89c81cc3dfeca8509aeff897c6edbd7d53c5 /src/theory/model.cpp
parentc7d04993e8d73105d091e0b732ddb63131b431a3 (diff)
minor fix for mbqi in finite model finding
Diffstat (limited to 'src/theory/model.cpp')
-rw-r--r--src/theory/model.cpp1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/theory/model.cpp b/src/theory/model.cpp
index bd9e6aefa..4a3ddc9ca 100644
--- a/src/theory/model.cpp
+++ b/src/theory/model.cpp
@@ -604,6 +604,7 @@ void TheoryEngineModelBuilder::buildModel(Model* m, bool fullModel)
Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, std::map< Node, Node >& constantReps)
{
+ Trace("tembn") << "Normalize " << r << std::endl;
std::map<Node, Node>::iterator itMap = constantReps.find(r);
if (itMap != constantReps.end()) {
return (*itMap).second;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback