Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

# PVS Bug 745

```Synopsis:        musimp causing segmentation violation
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri Feb 21 18:35:01 2003
Originator:      Paul Jackson
Organization:    inf.ed.ac.uk
Release:         PVS 3.0
Environment:
System:
Architecture:

Description:
Am using default PVS installation at SRI CSL:

PVS Version 3.1
Allegro CL Enterprise Edition
6.2 [Linux (x86)] (Feb 14, 2003 18:42)

Consider theory:

mu_exp : THEORY
BEGIN
State : TYPE = upto(4)

x,y : VAR State
N(x,y) : bool =
x = 0  AND y = 1
OR x = 1 AND y = 2
OR x = 2 AND y = 1

I(x) : bool = x = 0

R : VAR pred[State]

a1 : LEMMA mu(lambda R: lambda x : I(x) OR Exists y : N(y,x) AND R(y))
(2)

END mu_exp

Running musimp on Lemma a1 yields:

pvs(58):

a1 :

|-------
{1}   mu(LAMBDA R: LAMBDA x: I(x) OR (EXISTS y: N(y, x) AND R(y)))(2)

Rule? (musimp)
~[mu b94.L b99,b100,b101.[L .b101?b100?b99?b102:b103:b99?b104:b105:b100?b99?b
106:b107:b99?b108:b109](b117,b116,b115,b114,b113,b112,b111,b110) + (E b118,b11
9,b120.(b120 + b119 + 1) & (~b120 + ~b119 & ~b118) & b121 & [mu_init]: Package
Added Relational variable `b124' to Ip.
Added Relational variable `b125' to Ip.
Added Relational variable `b126' to Ip.
Added Relational variable `b127' to Ip.
Added Relational variable `b128' to Ip.
Looking up Relational variable: `b124'.
Looking up Relational variable: `b125'.
Looking up Relational variable: `b126'.
Looking up Relational variable: `b127'.
Looking up Relational variable: `b128'.

Error: Received signal number 11 (Segmentation violation)
[condition type: synchronous-operating-system-signal]

Restart actions (select using :continue):
1: Abort entirely from this process.
[1] pvs(63): :bt
Evaluation stack:

run-musimp <-
(:internal musimp-fun 0) <- rule-apply <-
(method proofstepper (proofstate)) <- [... proofstepper ] <-
prove*-int <- prove* <- prove-decl-body <-
(method dpi-start* (# function)) <-
(method prove-decl (formula-decl)) <-
(method prove-decl :around ...) <-
(:internal (:effective-method 1 t ...) 0) <- [... prove-decl ] <-
(method prove (formula-decl)) <-
(:internal (:effective-method 1 t ...) 0) <- prove-file-at <- eval <-