Ivy script code-extraction fails in both `ivy1.7 and ivy1.8` but `Checks OK` and generates testing agent

[prpr2770]

For the below script, we obtain the following error when extracting code using the comand

$ ivyc target=test build=true isolate=iso_R test_me.ivy
...
test_me.ivy: line 76: error: Call out to righty.spec.flip may have visible effect on righty.spec.ball
test_me.ivy: line 76: referenced here
test_me.ivy: line 17: referenced here

However, when compiling it to generate a randomized test-agent, it compiles correctly and produces an executable:

$ ivyc target=test build=true isolate=iso_right test_me.ivy 
g++  -I /home/user/.local/lib/python2.7/site-packages/ivy/include -L /home/user/.local/lib/python2.7/site-packages/ivy/lib -Wl,-rpath=/home/user/.local/lib/python2.7/site-packages/ivy/lib -g -o test_me test_me.cpp -lz3 -pthread
...
$ ./test_me true
...
< righty.impl.debug.send(74,msg_ping)
> righty.impl.trans.recv(1,msg_ping)
< righty.impl.debug.recv(1,msg_ping)
> righty.impl.trans.recv(2,msg_pong)
< righty.impl.debug.recv(2,msg_pong)
> righty.impl.trans.recv(2,msg_pong)
< righty.impl.debug.recv(2,msg_pong)
> righty.spec.hit(61)
< righty.impl.trans.send(61,61,msg_pong)
< righty.impl.debug.send(61,msg_pong)
> righty.spec.hit(87)
< righty.impl.trans.send(87,87,msg_ping)
< righty.impl.debug.send(87,msg_ping)
> righty.impl.trans.recv(1,msg_ping)
< righty.impl.debug.recv(1,msg_ping)
> righty.spec.hit(151)
< righty.impl.trans.send(151,151,msg_ping)
< righty.impl.debug.send(151,msg_ping)
> righty.spec.hit(128)
< righty.impl.trans.send(128,128,msg_pong)
< righty.impl.debug.send(128,msg_pong)
> righty.spec.hit(219)
< righty.impl.trans.send(219,219,msg_ping)
< righty.impl.debug.send(219,msg_ping)
> righty.spec.hit(86)
< righty.impl.trans.send(86,86,msg_pong)
< righty.impl.debug.send(86,msg_pong)
test_completed

The script is provided below:

#lang ivy1.7

include udp

type message_t = {msg_ping, msg_pong}

# ------ DEBUGGING 

module debugmod(node, msgtype, udp) = {
    action send(dst:node,m:msgtype)
    action recv(dts:node,m:msgtype)
    before udp.send(src:node,dst:node,msg:msgtype) {
        call send(dst,msg)
    }
    before udp.recv(dst:node,msg:msgtype) {
        call recv(dst,msg)
    }
}

module nodule = {
    type this

    implementation{

        interpret this -> bv[8]

    }

    isolate iso_node = this

}

instance node : nodule

module player = {

    object spec={

        parameter ball : bool

        action hit(me:node)

        #after init(me:node) { ball := true; }    

        action flip(me:node)={
            ball := ~ball;
        }    

    }

    object impl = {
        instance trans: udp_simple2(node, message_t)
        instance debug : debugmod(node, message_t, trans)

        implement spec.hit(me:node) {
            if (spec.ball ) {

                call trans.send(me, me, msg_ping); # #call intf.ping; # call transferred to reception.
                call spec.flip(me);
            }else{

                call trans.send(me, me, msg_pong); # #call intf.ping; # call transferred to reception.
                call spec.flip(me);
            }
        }

        implement trans.recv(dst:node, v:message_t){

            if (v = msg_ping  &  ~spec.ball ){

                call spec.flip(dst);

            }else if (v = msg_pong  &  spec.ball ){

                call spec.flip(dst);

            };

        }
    }

}

instance righty : player

export righty.spec.hit

import righty.impl.debug.send
import righty.impl.debug.recv

isolate iso_right = righty with node, message_t

extract iso_R(me:node) = righty(me), node, message_t