diff options
| author | Tim King <taking@cs.nyu.edu> | 2012-06-25 16:00:21 +0000 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2012-06-25 16:00:21 +0000 |
| commit | 43b978c7f326cb8d34b5b87d9bdbe9955397d1ce (patch) | |
| tree | 8e52fb48c2ddf8df79fe24b9b47593a1a4cf4d1e /src | |
| parent | 84c4269f3b9edb8de4134fe464dfc70679da2bb1 (diff) | |
Added a warning to arithmetic for a known dio solver bug. Somehow the fix never made it to trunk. Do not know how. The fix to the bug is pending the hunt for bug 363.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/arith/dio_solver.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/theory/arith/dio_solver.cpp b/src/theory/arith/dio_solver.cpp index 1ad6dd395..093fef0d5 100644 --- a/src/theory/arith/dio_solver.cpp +++ b/src/theory/arith/dio_solver.cpp @@ -213,6 +213,9 @@ Node DioSolver::proveIndex(TrailIndex i){ Node input = proofVariableToReason(v); Assert(acceptableOriginalNodes(input)); if(input.getKind() == kind::AND){ + if(input.getNumChildren() != 2){ + Warning() << "Fix this bug!" << std::endl; + } nb << input[0] << input[1]; }else{ nb << input; |