mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix build warnings

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-09-30 15:51:48 -07:00
parent 551cc53a2f
commit 86b97186b0
2 changed files with 11 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

26
src/muz/fp/datalog_parser.cpp
View file

@ -228,20 +228,20 @@ public:
class dlexer {
std::istream* m_input;
char_reader* m_reader;
char m_prev_char;
char m_curr_char;
int m_line;
int m_pos;
int m_tok_pos;
std::istream* m_input = nullptr;
char_reader* m_reader = nullptr;
int m_prev_char = 0;
int m_curr_char = 0;
int m_line = 1;
int m_pos = 0;
int m_tok_pos = 0;
string_buffer<> m_buffer;
reserved_symbols m_reserved_symbols;
public:
//when parsing domains, we want '.' character to be allowed in IDs, but elsewhere
//we don't (because of the "y." in rules like "P(x,y):-x=y.")
bool m_parsing_domains;
bool m_parsing_domains = false;
bool eos() const {
return m_curr_char == EOF;
@ -267,15 +267,7 @@ public:
next();
}
dlexer():
m_input(nullptr),
m_reader(nullptr),
m_prev_char(0),
m_curr_char(0),
m_line(1),
m_pos(0),
m_tok_pos(0),
m_parsing_domains(false) {
dlexer() {
}
void set_stream(std::istream* s, char_reader* r) {

2
src/smt/theory_str.cpp
View file

@ -4089,6 +4089,7 @@ namespace smt {
expr_ref_vector arrangement_disjunction(mgr);
int pos = 1;
(void)pos;
for (unsigned int i = 0; i <= strValue.length(); i++) {
zstring part1Str = strValue.extract(0, i);
zstring part2Str = strValue.extract(i, strValue.length() - i);
@ -4522,6 +4523,7 @@ namespace smt {
expr_ref_vector arrangement_disjunction(mgr);
int pos = 1;
(void)pos;
if (!avoidLoopCut || !has_self_cut(m, y)) {
expr_ref_vector and_item(mgr);