diff options
author | Tim King <taking@cs.nyu.edu> | 2012-06-14 20:59:14 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-06-14 20:59:14 +0000 |
commit | 66033cd2059d817cdeab5adc25f1397532a3fa78 (patch) | |
tree | 21aea6e8862c3868d5cecc449c951d64350dcca9 /src/theory/arith/congruence_manager.h | |
parent | 2211b6969c43436eb25b003bbeae7494217777c8 (diff) |
Fixing a bug related to explaining propagations with non-normalized witnesses.
Diffstat (limited to 'src/theory/arith/congruence_manager.h')
-rw-r--r-- | src/theory/arith/congruence_manager.h | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/src/theory/arith/congruence_manager.h b/src/theory/arith/congruence_manager.h index 1864bc89e..fd8eef1f1 100644 --- a/src/theory/arith/congruence_manager.h +++ b/src/theory/arith/congruence_manager.h @@ -152,6 +152,15 @@ private: ++(d_statistics.d_propagations); } + void pushBack(TNode n, TNode r, TNode w){ + d_explanationMap.insert(w, d_propagatations.size()); + d_explanationMap.insert(r, d_propagatations.size()); + d_explanationMap.insert(n, d_propagatations.size()); + d_propagatations.enqueue(n); + + ++(d_statistics.d_propagations); + } + bool propagate(TNode x); void explain(TNode literal, std::vector<TNode>& assumptions); |