Message structures compile correctly, but the up-cast/down-cast functionality of generator causes errors

[prpr2770]

The following message structure compiles correctly in the ivy-compiler.

#lang ivy1.7

type choice_response_request_type

object response_type_num = {
	variant this of choice_response_request_type
}

object request_type_num = {
	variant this of choice_response_request_type
}


type message_block

type response_type = {res1, res2, res3}
type request_type = {req1, req2, req3, req4}

object response_block = {
	variant this of message_block = struct{
		load : response_type,
		val : choice_response_request_type
	}
}

object request_block = {
	variant this of message_block = struct{
		load : request_type,
		val : choice_response_request_type
	}
}


interpret choice_response_request_type -> int
interpret response_type_num -> int
interpret request_type_num -> int

However, when the above messages are used inside an application, the generator throws up an error. From the logs, I feel there an error in the up-cast/down-cast of choice_response_request_type into either response_type_num or request_type_num.

I obtain the following logs:

ivyc target=test message_app10A.ivy 
Traceback (most recent call last):
  File "/home/user/.local/bin/ivyc", line 11, in <module>
    sys.exit(ivyc())
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_to_cpp.py", line 5717, in ivyc
    main_int(True)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_to_cpp.py", line 5838, in main_int
    header,impl = module_to_cpp_class(classname,basename)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_to_cpp.py", line 3354, in module_to_cpp_class
    emit_action_gen(sf,impl,name,action,classname)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_to_cpp.py", line 1740, in emit_action_gen
    impl.append('add("(assert {})");\n'.format(slv.formula_to_z3(pre).sexpr().replace('|!1','!1|').replace('\\|','').replace('\n',' "\n"')))
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 536, in formula_to_z3
    z3_fmla = formula_to_z3_closed(fmla)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 525, in formula_to_z3_closed
    z3_formula = formula_to_z3_int(fmla)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 494, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 494, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 494, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 494, in formula_to_z3_int
    args = [formula_to_z3_int(arg) for arg in fmla.args]
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 491, in formula_to_z3_int
    return atom_to_z3(fmla)
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 407, in atom_to_z3
    rel = lookup_native(atom.relname,relations,"relation")
  File "/home/user/.local/lib/python2.7/site-packages/ivy/ivy_solver.py", line 247, in lookup_native
    raise iu.IvyError(None,'{} is not a supported Z3 {}'.format(name,kind))
NameError: global name 'name' is not defined

for the application developed below:

#lang ivy1.7

include messageIEC


object intf = {
    action send(x:message_block)
	action recv(x:message_block)
    
    }


object spec = {
    relation sent(X:message_block)

    after init {
        sent(X) := false
    }

    before intf.send {
        sent(x) := true
    }

    before intf.recv {
        assert sent(x)
    }
}

object protocol = {
    implement intf.send {
        call intf.recv(x)
    }
}

import intf.recv
export intf.send