summaryrefslogtreecommitdiff
path: root/src/theory/arith/arith_utilities.h
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2010-11-09 21:57:06 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2010-11-09 21:57:06 +0000
commitdf5f7fe03fda041429548bcb39abb8916ca2e291 (patch)
tree46b08f3e35ee9c3d4c551d82f3e7e36582383f39 /src/theory/arith/arith_utilities.h
parent1f07775e9205b3f9e172a1ad218a9015b7265b58 (diff)
Lemmas on demand work, push-pop, some cleanup.
Diffstat (limited to 'src/theory/arith/arith_utilities.h')
-rw-r--r--src/theory/arith/arith_utilities.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index d50c48552..25aff4e75 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -237,10 +237,12 @@ inline int deltaCoeff(Kind k){
case kind::EQUAL:
return kind::DISTINCT;
default:
+ Unreachable();
return kind::UNDEFINED_KIND;
}
}
default:
+ Unreachable();
return kind::UNDEFINED_KIND;
}
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback