diff options
| author | lianah <lianahady@gmail.com> | 2013-03-24 18:50:39 -0400 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2013-03-24 18:50:39 -0400 |
| commit | ab19f7ee3cd09d9e9bbf3a75f54989e132442ccf (patch) | |
| tree | c0809a804105310f55f225bb4a2e5996ebb693b0 /src/theory/bv/slicer.cpp | |
| parent | b9b17625957d2e718dc2d071dff505d04ccad879 (diff) | |
incremental inequality solver implemented
Diffstat (limited to 'src/theory/bv/slicer.cpp')
| -rw-r--r-- | src/theory/bv/slicer.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/bv/slicer.cpp b/src/theory/bv/slicer.cpp index b24702635..5382695cf 100644 --- a/src/theory/bv/slicer.cpp +++ b/src/theory/bv/slicer.cpp @@ -589,8 +589,8 @@ void UnionFind::ensureSlicing(TermId t) { void UnionFind::backtrack() { int size = d_undoStack.size(); for (int i = size; i > (int)d_undoStackIndex.get(); --i) { - Operation op = d_undoStack.back(); Assert (!d_undoStack.empty()); + Operation op = d_undoStack.back(); d_undoStack.pop_back(); if (op.op == UnionFind::MERGE) { undoMerge(op.id); |