2

I developed a model using Z3 .Net API. The program runs well. But when I increase the input size (i.e., the model size), the program runs for a long time and then it ends giving the following message:

"Unhandled Exception: OutOfMemoryException."

I am wonderding is there any way I can increase the memory size for the program.

pad
  • 41,040
  • 7
  • 92
  • 166
Ashiq
  • 307
  • 2
  • 10

1 Answers1

2

If you're compiling to x86 platform, you're hitting 2GB memory limit of 32-bit processes. If you're targeting x64, there is also 2GB limit of .NET objects which you cannot bypass. In my experience, this 2GB limit is enough under normal circumstances.

You have a choice of running Z3 executable using .NET and redirecting output string to handle it by yourself. As a last resort, you can rewrite the memory-critical part in your program using Z3 C API to bypass above restrictions, which I think you may not want to do.

Community
  • 1
  • 1
pad
  • 41,040
  • 7
  • 92
  • 166
  • Can you explain little more about "you have a choice of running Z3 executable using .NET and redirecting output string to handle it by yourself"? Moreover, one of my fellow researcher has told me that "Yices" do not have this kind of limit. Isn't it possible to let Z3 use all available memory? – Ashiq Oct 12 '12 at 10:36
  • What I meant is to run `Z3.exe` as an external process using `Process` class in .NET. That's the way [VCC/Boogie](http://vcc.codeplex.com/SourceControl/changeset/view/1cc7534886db) using Z3. Yices doesn't have that problem because Yices doesn't have APIs on .NET platform which has inherent restrictions. – pad Oct 12 '12 at 10:58