When defining loans in OpaqueLoan::define, if there are no loans defined (as represented by the Rvalues::borrow_typelabs() iterator), then Z3 crashes because there are no variants defined.
I haven’t been able to figure out how to introduce a loan into the code. I’ve tried code such as
int foo(int* x) {
if (x > 0) {
return foo(x - 1);
} else {
return *x;
}
}
int main() {
int x = 0;
return foo(&x);
}
but I haven’t been able to get anything working.
How do I ensure that at least 1 opaque loan is defined?
Also, as a side note, I can’t just define it if there is at least 1 variant since the datatype is expected to be present later in the program.