bad recursive function definition not (apparently) available

[viper-admin]

Created by @MartinClochard on 2018-05-08 15:17 Last updated on 2018-05-09 15:42

Against expectations, the following assertion about an ill-defined recursive function is not proved:

#!scala

function wild() : Int { 1 + wild() }
method fail () { assert wild() == 1 + wild() }

Note that splitting the ill-defined recursive function in two parts works, as in:

#!scala

function wild() : Int { 1 + wild2() }
function wild2() : Int { 1 + wild() }
method fail () { assert wild() == 1 + wild2(); assert wild() == 1 + wild() }

[viper-admin]

@alexanderjsummers on 2018-05-08 16:02:

• edited the title
• edited the description

[viper-admin]

@alexanderjsummers on 2018-05-08 16:03:

• edited the description

[viper-admin]

@alexanderjsummers commented on 2018-05-08 16:04

See also the same Silicon issue

[viper-admin]

@alexanderjsummers commented on 2018-05-09 15:42

See this Z3 Stackoverflow post