diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-11-26 17:30:44 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-11-26 17:30:44 +0000 |
| commit | c3ca3d8c58cc9954f8ad190e1e2dedbcbb5372f0 (patch) | |
| tree | 4830fb02118a499da8cb62aaec06b16919e0d05a /src/theory/arith/dio_solver.h | |
| parent | 2a731b9164bb178f1232a9af0babc7dd84450cea (diff) | |
Removing DioSolver::acceptableOriginalNodes(). This assertion was too strong, and was broken by r4620. This commit resolves bug463. Adding a previously triggering test case.
Diffstat (limited to 'src/theory/arith/dio_solver.h')
| -rw-r--r-- | src/theory/arith/dio_solver.h | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index 7d1faed86..bfcd19021 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -237,11 +237,6 @@ private: */ size_t allocateVariableInPool(); - /** - * Returns true if the node can be accepted as a reason according to the - * kinds. - */ - bool acceptableOriginalNodes(Node n); /** Empties the unproccessed input constraints into the queue. */ void enqueueInputConstraints(); |