na

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
Z3Prover · Apr 15, 2020 · 2e1e9c9 · 2e1e9c9
1 parent 3845e08
commit 2e1e9c9
Show file tree

Hide file tree

Showing 3 changed files with 2 additions and 2 deletions.
diff --git 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<rational> & 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
@@ -13,6 +13,7 @@ Module Name:
 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
@@ -17,10 +17,10 @@ Module Name:
 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_