`ivy_to_cpp` and `ivyc` don't seem to handle enumerative interpretations correctly

[hidenori-shinohara]

#lang ivy1.7    
type id_t    
interpret id_t -> {id0, id1}    
object myObject = {    
    action myAction(x:id_t) = {    
        require x = id0;    
    }    
    invariant forall X:id_t. X = id0 | X = id1    
}    
export myObject.myAction    
extract runner = myObject

This can be verified by the command ivy_check test.ivy, and that makes me think that I don't have typos in this. However, when I convert this into C++ using ivyc target=test isolate=runner classname=test test.ivy, it creates C++ code that contains id0 in it without defining what id0 is. This leads to C++ compilation errors. For instance, the following is the error message that I got:

g++  -I /usr/local/lib/python2.7/dist-packages/ivy/include -L /usr/local/lib/python2.7/dist-packages/ivy/lib -Wl,-rpath=/usr/local/lib/python2.7/dist-packages/ivy/lib -g -o test test.cpp -lz3 -pthread
test.cpp: In member function ‘virtual void test::ext__myObject__myAction(unsigned int)’:
test.cpp:1115:26: error: ‘id0’ was not declared in this scope
 1115 |         ivy_assume((x == id0), "test.ivy: line 9");
     |                          ^~~
test.cpp: In member function ‘virtual bool ext__myObject__myAction_gen::generate(test&)’:
test.cpp:1198:19: error: ‘id0’ is not a member of ‘test’
 1198 |         x = test::id0;
      |      

Similarly, when I try to make executables using

ivy_to_cpp target=repl isolate=runner test.ivy    
g++ -O2 test.cpp -pthread -lpthread -o test

I also get an error of the same nature.

test.cpp: In member function ‘virtual void test::ext__myObject__myAction(unsigned int)’:
test.cpp:590:26: error: ‘id0’ was not declared in this scope
  590 |         ivy_assume((x == id0), "test.ivy: line 9");
      |                          ^~~