summaryrefslogtreecommitdiff
path: root/src/prop/theory_proxy.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-10-06 18:53:27 +0000
committerMorgan Deters <mdeters@gmail.com>2012-10-06 18:53:27 +0000
commit4e883ffc0b88256a966183ac6b87bb5767154cdf (patch)
treea193f12035e4417834ef08312f50739ae0b39a87 /src/prop/theory_proxy.cpp
parent99cad5495be99efae434177d1537d4cfac35581c (diff)
* Clean up some options documentation
* Remove defunct --no-theory-registration option * Point people to Wiki tutorial * Modernize the cut-release script * Misc cleanup, documentation (this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'src/prop/theory_proxy.cpp')
-rw-r--r--src/prop/theory_proxy.cpp3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 9ed2202fe..1434cf6c7 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -28,6 +28,7 @@
#include "decision/options.h"
#include "util/lemma_input_channel.h"
#include "util/lemma_output_channel.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
namespace prop {
@@ -170,11 +171,11 @@ SatLiteral TheoryProxy::getNextReplayDecision() {
Expr e = options::replayStream()->nextExpr();
if(!e.isNull()) { // we get null node when out of decisions to replay
// convert & return
+ ++d_replayedDecisions;
return d_cnfStream->getLiteral(e);
}
}
#endif /* CVC4_REPLAY */
- //FIXME!
return undefSatLiteral;
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback