mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

fix #2714

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-11-21 16:37:45 -08:00
parent 8db0429809
commit b2c3025e21
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/smt_conflict_resolution.cpp
View file

@ -363,8 +363,7 @@ namespace smt {
}
idx--;
// skip literals from levels above the conflict level
while (m_ctx.get_assign_level(m_assigned_literals[idx]) > m_conflict_lvl) {
SASSERT(idx > 0);
while (m_ctx.get_assign_level(m_assigned_literals[idx]) > m_conflict_lvl && idx > 0) {
idx--;
}
return idx;

2
src/smt/theory_str.cpp
View file

@ -4284,6 +4284,7 @@ namespace smt {
// adding length constraint for _ = constStr seems slowing things down.
expr_ref option1(mk_and(and_item), mgr);
ctx.get_rewriter()(option1);
arrangement_disjunction.push_back(option1);
double priority;
if (i == strValue.length()) {
@ -7681,7 +7682,6 @@ namespace smt {
void theory_str::add_theory_assumptions(expr_ref_vector & assumptions) {
TRACE("str", tout << "add overlap assumption for theory_str" << std::endl;);
const char* strOverlap = "!!TheoryStrOverlapAssumption!!";
seq_util m_sequtil(get_manager());
sort * s = get_manager().mk_bool_sort();
m_theoryStrOverlapAssumption_term = expr_ref(mk_fresh_const(strOverlap, s), get_manager());
assumptions.push_back(get_manager().mk_not(m_theoryStrOverlapAssumption_term));