1

Closed

Segfault in latest version of Z3

description

Hello,

The following (minimized) SMT file causes a segfault for me in version 4.3.1 of Z3 when run on 64 bit Ubuntu.

matt@ubappy:~/scratch$ uname -a
Linux ubappy 3.2.0-31-generic #50-Ubuntu SMP Fri Sep 7 16:16:45 UTC 2012 x86_64 x86_64 x86_64 GNU/Linux
matt@ubappy:~/scratch$ z3 -version
Z3 version 4.3.1
matt@ubappy:~/scratch$ z3 z3_crash_min.smt
Segmentation fault (core dumped)
matt@ubappy:~/scratch$

Cheers,
Matt

file attachments

Closed Dec 9, 2012 at 7:32 PM by leodemoura
The segfault has been fixed.

comments

leodemoura wrote Nov 29, 2012 at 5:27 PM

This bug has already been fixed in the "unstable" branch, and will be available in the next release.

Z3 4.3.1 may crash in sort incorrect or syntactically incorrect formulas. If we use the Z3 from the "unstable" branch we get the error

ERROR: select takes at least two arguments

The problem is on line 26
select nondet_symex.Snondet270 (

It seems there is a missing '('

BTW, consider moving to SMT-LIB 2.0 :-)
It provides many extra features and much better error report.

leodemoura wrote Nov 29, 2012 at 5:27 PM

The bug has already been fixed in the "unstable" branch. The fix will be available in the next release.

** Closed by leodemoura 11/29/2012 10:27AM

mattlewis wrote Nov 29, 2012 at 7:11 PM

Thanks for the quick reply, Leo. I'm afraid I minimized my original crashing input fairly naively & that apparently masked the real crash. I'm attaching the original (unminimized) input, which also segfaults 4.3.2.

I keep meaning to switch to SMT-LIB 2.0, thanks for reminding me!

mattlewis wrote Nov 29, 2012 at 7:11 PM

I've attached the un-minimized input, which segfaults Z3 4.3.2.

leodemoura wrote Nov 30, 2012 at 3:56 AM

I will investigate the issue.

Btw, keep in mind that the unstable branch is constantly being modified. Thus, the version number is not very informative. Please consider using the git hash when reporting problems with the unstable.

Thanks,
Leo

leodemoura wrote Dec 9, 2012 at 7:32 PM

I fixed the problem. The fix is already available in the unstable branch.
http://z3.codeplex.com/SourceControl/changeset/33234a4162ed

Sign in to add a comment