mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix segfault #2360
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
6f08c0788f
commit
1f0d162b7f
|
@ -5964,7 +5964,7 @@ void theory_seq::add_lt_axiom(expr* n) {
|
|||
*/
|
||||
void theory_seq::add_le_axiom(expr* n) {
|
||||
expr* e1 = nullptr, *e2 = nullptr;
|
||||
VERIFY(m_util.str.is_lt(n, e1, e2));
|
||||
VERIFY(m_util.str.is_le(n, e1, e2));
|
||||
literal lt = mk_literal(m_util.str.mk_lex_lt(e1, e2));
|
||||
literal le = mk_literal(n);
|
||||
literal eq = mk_eq(e1, e2, false);
|
||||
|
|
Loading…
Reference in a new issue