diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4125e9cc1..dca1bbce2 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -1640,7 +1640,6 @@ bool theory_seq::enforce_length(expr_ref_vector const& es, vector & le len.push_back(rational(s.length())); } else if (get_length(e, val)) { - SASSERT(!val.is_neg()); len.push_back(val); } else { diff --git a/src/util/buffer.h b/src/util/buffer.h index 13a5ca00b..cd8c1d4ac 100644 --- a/src/util/buffer.h +++ b/src/util/buffer.h @@ -13,6 +13,7 @@ Abstract: Author: Leonardo de Moura (leonardo) 2006-10-16. + Daniel Schemmel 2019-2-23 Revision History: diff --git a/src/util/vector.h b/src/util/vector.h index f94fda4f0..5dfb199a4 100644 --- a/src/util/vector.h +++ b/src/util/vector.h @@ -17,10 +17,10 @@ Abstract: Author: Leonardo de Moura (leonardo) 2006-09-11. + Daniel Schemmel 2019-2-23 Revision History: - 2019-2-23 Renamed from vector to vector to provide new implementation --*/ #ifndef VECTOR_H_