#66676 closed defect (fixed)

Z3 SMT solver crashes

Reported by: mouse07410 (Mouse) Owned by: catap (Kirill A. Korinsky)
Priority: Normal Milestone:
Component: ports Version:
Keywords: Cc: landonf (Landon Fuller)
Port: z3

Description

macOS Monterey 12.6.2, Xcode-14.2.

Reproducer (file test2.smt):

(set-option :print-success true )
(set-option :produce-models true )
(set-option :global-decls false )
(push 1 )

Invocation:

$ z3 -smt2 test2.smt 
success
success
success
Segmentation fault: 11
$ 

Crash report:

Termination Reason:    Namespace SIGNAL, Code 11 Segmentation fault: 11
Terminating Process:   exc handler [58074]

VM Region Info: 0 is not in any region.  Bytes before following region: 4382007296
      REGION TYPE                    START - END         [ VSIZE] PRT/MAX SHRMOD  REGION DETAIL
      UNUSED SPACE AT START
--->  
      __TEXT                      105302000-10689a000    [ 21.6M] r-x/r-x SM=COW  .../local/bin/z3

Thread 0 Crashed::  Dispatch queue: com.apple.main-thread
0   z3                            	       0x106198c80 smt::theory_seq::theory_seq(smt::context&) + 192
1   z3                            	       0x105f55e39 smt::setup::setup_seq_str(static_features const&) + 265
2   z3                            	       0x105f516a0 smt::setup::setup_unknown() + 384
3   z3                            	       0x105ef95e5 smt::context::setup_context(bool) + 149
4   z3                            	       0x105ef570d smt::context::push() + 61
5   z3                            	       0x105a78908 solver_na2as::push() + 40
6   z3                            	       0x105a9984d cmd_context::push() + 2205
7   z3                            	       0x105ac6268 smt2::parser::operator()() + 4312
8   z3                            	       0x10672f693 read_smtlib2_commands(char const*) + 563
9   z3                            	       0x10672cfa3 main + 2115
10  dyld                          	       0x10c83352e start + 462

Also, the current Z3 version released in Sep 2022 is 4.11.2. This port is still at 4.8.17 - it would be nice to upgrade.

Change History (1)

comment:1 Changed 21 months ago by catap (Kirill A. Korinsky)

Owner: set to catap
Resolution: fixed
Status: newclosed

In c307ae9e65c2b65493fe065083b6274edc0ea37d/macports-ports (master):

z3: update to 4.12.1; add py311; remove py27

Made port lint --nitpick almost happy

Closes: #66676

Note: See TracTickets for help on using tickets.