diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-13 18:27:11 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-21 16:25:13 -0400 |
| commit | 2a2c5102e10a8b3f1091bc50916fda5e766b5d4a (patch) | |
| tree | e358fead2796386ed99fece5f964643b6979a4df /src/theory/arith/arith_rewriter.cpp | |
| parent | ed40bbae19622ff29e1ca6eb873d20262ed21926 (diff) | |
Better error in case of nonlinear assertions while in linear logic
Diffstat (limited to 'src/theory/arith/arith_rewriter.cpp')
| -rw-r--r-- | src/theory/arith/arith_rewriter.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp index 823b61df5..ee9ff9e1b 100644 --- a/src/theory/arith/arith_rewriter.cpp +++ b/src/theory/arith/arith_rewriter.cpp @@ -86,7 +86,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ }else if(t.isVar()){ return rewriteVariable(t); }else{ - switch(t.getKind()){ + switch(Kind k = t.getKind()){ case kind::MINUS: return rewriteMinus(t, true); case kind::UMINUS: @@ -104,7 +104,7 @@ RewriteResponse ArithRewriter::preRewriteTerm(TNode t){ case kind::INTS_MODULUS_TOTAL: return rewriteIntsDivModTotal(t,true); default: - Unreachable(); + Unhandled(k); } } } |