mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 23:26:30 +00:00
Code Activity

Removed assertion to make the build dependencies acyclic

Browse source
This commit is contained in:
CEisenhofer 2026-06-03 10:58:25 +02:00
parent 3908016651
commit e94b6db8e5
2 changed files with 8 additions and 14 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/seq/seq_nielsen.cpp
View file

@ -35,14 +35,12 @@ NSB review:
#include "ast/rewriter/th_rewriter.h"
#include "ast/rewriter/seq_skolem.h"
#include "ast/rewriter/var_subst.h"
#include "smt/smt_enode.h"
#include "util/statistics.h"
#include <algorithm>
#include <complex>
#include <cstdlib>
#include <stack>
#include <unordered_map>
#include <vector>
namespace seq {
@ -54,7 +52,6 @@ namespace seq {
for (dep_source const &d : vs) {
if (std::holds_alternative<enode_pair>(d)) {
eqs.push_back(std::get<enode_pair>(d));
SASSERT(eqs.back().first->get_root() == eqs.back().second->get_root());
}
else if (std::holds_alternative<sat::literal>(d))
lits.push_back(std::get<sat::literal>(d));

19
src/smt/seq/seq_nielsen.h
View file

@ -232,24 +232,21 @@ Author:
#pragma once
#include "util/vector.h"
#include "util/uint_set.h"
#include "util/dependency.h"
#include "util/map.h"
#include "util/lbool.h"
#include "util/rational.h"
#include "ast/ast.h"
#include "ast/seq_decl_plugin.h"
#include "ast/arith_decl_plugin.h"
#include "ast/euf/euf_sgraph.h"
#include <map>
#include "model/model.h"
#include "util/lbool.h"
#include "util/dependency.h"
#include "util/map.h"
#include "util/obj_ref_hashtable.h"
#include "util/uint_map.h"
#include "util/rational.h"
#include "util/uint_set.h"
#include "util/vector.h"
#include <map>
namespace smt {
class enode;
}
namespace smt { class enode; }
namespace seq {