diff options
| author | Tim King <taking@cs.nyu.edu> | 2014-02-19 15:50:07 -0500 |
|---|---|---|
| committer | Tim King <taking@cs.nyu.edu> | 2014-02-19 15:50:07 -0500 |
| commit | cca221de7d29e86fd770af3aca0efc0d877dff26 (patch) | |
| tree | 661a5b911f467064ffa9417c77f68bcc086910e6 /src/theory/arith/dio_solver.h | |
| parent | 218dbfa797e6318484f7f858a29dd4c422bc37d3 (diff) | |
Stopping non-linear terms from entering the dio solver. Fixes bug 547.
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); |