bad recursive function definition not (apparently) available

[viper-admin]

Created by @alexanderjsummers on 2018-05-08 16:03
Last updated on 2018-06-03 10:51

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 commented on 2018-05-08 16:05

See also the same Carbon issue

[viper-admin]

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

See this Z3 Stackoverflow post

[viper-admin]

@mschwerhoff on 2018-06-03 10:51:

• changed component from (none) to Z3