mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 14:17:47 +00:00
Code Activity

fix crash with D:\\bench\\inputs\\QF_S\\20240318-omark\\cyclic-xy.smt2

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-05-05 10:53:12 -07:00
parent b65f22ef3b
commit 8c02ec087b
1 changed files with 6 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -640,7 +640,12 @@ namespace seq {
bool upper_bound(expr* e, rational& up, dep_tracker& dep); bool upper_bound(expr* e, rational& up, dep_tracker& dep);
// character constraint access (mirrors ZIPT's CharRanges) // character constraint access (mirrors ZIPT's CharRanges)
u_map<std::pair<char_set, dep_tracker>> char_ranges() const { return m_char_ranges; } u_map<std::pair<char_set, dep_tracker>>& char_ranges() { return m_char_ranges; }
u_map<std::pair<char_set, dep_tracker>> const &char_ranges() const {
return m_char_ranges;
}
// add a character range constraint for a symbolic char. // add a character range constraint for a symbolic char.
// intersects with existing range; sets conflict if result is empty. // intersects with existing range; sets conflict if result is empty.