diff options
Diffstat (limited to 'src/theory/arith/dio_solver.h')
| -rw-r--r-- | src/theory/arith/dio_solver.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/arith/dio_solver.h b/src/theory/arith/dio_solver.h index f19291c98..5039f826c 100644 --- a/src/theory/arith/dio_solver.h +++ b/src/theory/arith/dio_solver.h @@ -191,6 +191,8 @@ public: * orig can either be of the form (= p c) or (and ub lb). * where ub is either (leq p c) or (not (> p [- c 1])), and * where lb is either (geq p c) or (not (< p [+ c 1])) + * + * If eq cannot be used, this constraint is dropped. */ void pushInputConstraint(const Comparison& eq, Node reason); |