From 85fd139c7f7cb363fc35793e55acbd4465b58853 Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Thu, 13 Feb 2020 14:43:09 -0500 Subject: [PATCH] z3str3: assert precondition for regex linearity axiom --- src/smt/theory_str_regex.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_str_regex.cpp b/src/smt/theory_str_regex.cpp index 518da6804..0f6b7e4cb 100644 --- a/src/smt/theory_str_regex.cpp +++ b/src/smt/theory_str_regex.cpp @@ -93,7 +93,8 @@ namespace smt { // generate new length constraint expr_ref_vector extra_length_vars(m); expr_ref _top_level_length_constraint = infer_all_regex_lengths(mk_strlen(str), re, extra_length_vars); - expr_ref top_level_length_constraint(_top_level_length_constraint, m); + expr_ref premise(str_in_re, m); + expr_ref top_level_length_constraint(m.mk_implies(premise, _top_level_length_constraint), m); th_rewriter rw(m); rw(top_level_length_constraint); TRACE("str", tout << "top-level length constraint: " << mk_pp(top_level_length_constraint, m) << std::endl;);