Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

.NET application crashes with memory access exception #7003

Closed
GennadyGS opened this issue Nov 19, 2023 · 2 comments
Closed

.NET application crashes with memory access exception #7003

GennadyGS opened this issue Nov 19, 2023 · 2 comments

Comments

@GennadyGS
Copy link

After updating to latest Z3 version (4.12.2) from version 4.11.2 application using .NET API crashes with error:

Fatal error. System.AccessViolationException: Attempted to read or write protected memory. This is often an indication that other memory is corrupt.
Repeat 2 times:
--------------------------------
   at Microsoft.Z3.Native+LIB.Z3_del_constructor(IntPtr, IntPtr)
--------------------------------
   at Microsoft.Z3.Native.Z3_del_constructor(IntPtr, IntPtr)
   at Microsoft.Z3.Constructor.Finalize()

As a result of investigation, I have discovered that it started to reproduce from version 4.12.0.

Here is the in simplest steps to reproduce, which I was able to found:

using System;
using Microsoft.Z3;

CreateConstructor();
GC.Collect();

void CreateConstructor()
{
    using var context = new Context();
    var constructor = context.MkConstructor("a", "a");
}

This sample does not reproduce the error stably, but for me at least more than in 50% cases, so it may require to run a couple of times.
Analyzing the changes between 4.11.2 and 4.12.0 I have suspicion that regression was introduced by PR #6361. Cannot verify this since I was not able to build Z3 solution on my machine following the instruction.

NikolajBjorner added a commit that referenced this issue Nov 19, 2023
minor tweaks to gomory and reset n3 within loop (but the entire function is dead code).
@NikolajBjorner
Copy link
Contributor

I will consider this as fixed.

@GennadyGS
Copy link
Author

It works.
Thanks!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants