issues
search
VeriFIT
/
z3-noodler
The Z3-Noodler String Solver
Other
6
stars
5
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
Keep conv axioms
#181
jurajsic
opened
1 day ago
0
Model of singleton automata
#180
jurajsic
opened
1 day ago
1
Implement model generation for cyclic inclusions
#179
jurajsic
opened
1 day ago
0
Conversion: fixing
#178
vhavlena
opened
3 days ago
0
Fixing axiomatization of predicates
#177
jurajsic
closed
3 days ago
1
Prefix: fixing the positive case
#176
vhavlena
closed
6 days ago
3
Invalid model
#175
jurajsic
opened
1 week ago
2
Concatenation model fix
#174
jurajsic
closed
1 week ago
2
Do not remove the same equation twice in preprocessing
#173
jurajsic
closed
1 week ago
4
Small refactoring in final_check
#172
jurajsic
closed
2 weeks ago
1
Fix axiomitizing conversions
#171
jurajsic
closed
2 weeks ago
2
README: publication update
#170
vhavlena
closed
2 weeks ago
0
Collecting statistics
#169
vhavlena
closed
2 weeks ago
5
not-contains: implement not-contains > LIA reduction
#168
MichalHe
opened
1 month ago
0
Length Decision Procedure: models
#167
vhavlena
closed
3 weeks ago
2
Nielsen: model generation updates
#166
vhavlena
closed
1 month ago
1
Fast models
#165
jurajsic
closed
1 month ago
4
`full_str_int`: performance optimizations
#164
vhavlena
closed
1 month ago
4
Relevancy fixing
#163
vhavlena
closed
1 month ago
4
Fix axioms for replace_re
#162
jurajsic
closed
1 month ago
3
Models for unary decision procedure
#161
vhavlena
closed
1 month ago
1
Further model generation fixes
#160
jurajsic
closed
1 month ago
4
Nielsen: model generation
#159
vhavlena
closed
2 months ago
9
Update to newest Mata
#158
jurajsic
closed
2 months ago
3
Bug for not contains
#157
jurajsic
closed
2 months ago
2
Model generation fixing
#156
jurajsic
closed
1 month ago
2
Determinization argument in `regex::conv_to_nfa` is not passed for concatenation
#155
jurajsic
opened
2 months ago
0
[WIP] Refactor preprocessing
#154
jurajsic
closed
1 month ago
0
Bug fixing: length unsat formula in preprocessing
#153
vhavlena
closed
2 months ago
3
Small cleaning in `final_check_eh`
#152
jurajsic
closed
3 months ago
4
Remove useless int variables for conversions
#151
jurajsic
closed
3 months ago
1
Not contains via counter automata
#150
vhavlena
closed
2 months ago
7
Support for (limited) model generation
#149
jurajsic
closed
2 months ago
6
SMT-COMP: minor
#148
vhavlena
closed
4 months ago
0
SMT-COMP fixing
#147
vhavlena
closed
4 months ago
0
SMT-COMP files
#146
vhavlena
closed
4 months ago
0
Multiple membership heuristic improvement
#145
jurajsic
closed
4 months ago
5
Add support for QF_SNIA
#144
jurajsic
closed
4 months ago
8
Length decision procedure
#143
vhavlena
closed
2 months ago
10
Length decision procedure
#142
xhrani03
closed
4 months ago
2
Fix invalid link to SMTLIB theory of strings
#141
Adda0
closed
4 months ago
0
Fixing infinite looping
#140
vhavlena
closed
4 months ago
1
Multiple regex membership heuristic
#139
jurajsic
closed
4 months ago
2
Move rewriter rule
#138
jurajsic
closed
1 month ago
0
Reenable rewriter rule `(str.in A (str.to_re B))` -> `(A = B)`
#137
jurajsic
closed
4 months ago
1
Nielsen optimizations
#136
vhavlena
closed
4 months ago
2
Incorrect result
#135
jurajsic
closed
2 weeks ago
1
Regex construction: optimizations
#134
vhavlena
closed
4 months ago
4
Update base Z3 to v4.13.0
#133
jurajsic
closed
5 months ago
7
Fix `to_int` computation so invalid cases are not used to generate numbers
#132
jurajsic
closed
6 months ago
1
Next