mirror of
https://github.com/Z3Prover/z3
synced 2025-04-24 17:45:32 +00:00
na
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
3845e0859c
commit
2e1e9c9082
3 changed files with 2 additions and 2 deletions
|
@ -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 {
|
||||
|
|
|
@ -13,6 +13,7 @@ Abstract:
|
|||
Author:
|
||||
|
||||
Leonardo de Moura (leonardo) 2006-10-16.
|
||||
Daniel Schemmel 2019-2-23
|
||||
|
||||
Revision History:
|
||||
|
||||
|
|
|
@ -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_
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue