mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

ADT-constructor generation crashed in .NET/Java when no (= default) fields are given (#6287)

Browse source
This commit is contained in:
Clemens Eisenhofer 2022-08-21 21:40:38 +02:00 • committed by GitHub
parent 6ba9ada1e2
commit 56fb161532
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/api/dotnet/Context.cs
View file

@ -124,7 +124,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
internal Symbol[] MkSymbols(string[] names) internal Symbol[] MkSymbols(string[] names)
{ {
if (names == null) return null; if (names == null) return new Symbol[0];
Symbol[] result = new Symbol[names.Length]; Symbol[] result = new Symbol[names.Length];
for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]); for (int i = 0; i < names.Length; ++i) result[i] = MkSymbol(names[i]);
return result; return result;

2
src/api/java/Context.java
View file

@ -110,7 +110,7 @@ public class Context implements AutoCloseable {
Symbol[] mkSymbols(String[] names) Symbol[] mkSymbols(String[] names)
{ {
if (names == null) if (names == null)
return null; return new Symbol[0];
Symbol[] result = new Symbol[names.length]; Symbol[] result = new Symbol[names.length];
for (int i = 0; i < names.length; ++i) for (int i = 0; i < names.length; ++i)
result[i] = mkSymbol(names[i]); result[i] = mkSymbol(names[i]);