rf_to_bv only considers architectures with 16 general-purpose registers

[GTP95]

Greetings,

in the sw_verifier project, inside the contract.h header file we have the following definition for the rf_to_bv macro:

#define rf_to_bv(r) r.x1, r.x2, r.x3, r.x4, r.x5, r.x6, r.x7, r.x8, r.x9, r.x10, r.x11, r.x12, r.x13, r.x14, r.x15

It seems to assume an ISA with 16 general-purpose registers (and skipping register 0, because it always returns 0). But, in other places, your code uses the RV_I flag to determine whether it should work with 16 or 32 registers. Why?
Thank you for the clarification,

GTP

[GTP95]

Looking again at the code, I think I got this wrong. But I'm still unsure about what this macro is doing. it now seems to me that it may be taking in the value of a register and return only bits 1 to 15, but why?

[thismusicdude]

oh you again? Did you get it up and running? @GTP95 LMAO

[GTP95]

Nope, and I'm not working on this anymore, as I left academia for the industry. I won't comment further on the status of research tools, as it would be off-topic here. I just suggest you to read this: https://dl.acm.org/doi/10.1145/3685699. Il Gio 20 Nov 2025, 02:13 Max Schmitt ***@***.***> ha scritto:

…

*thismusicdude* left a comment (isec-tugraz/glitch-contracts#2) <#2 (comment)> oh you again? Did you get it up and running? @GTP95 <https://github.com/GTP95> LMAO — Reply to this email directly, view it on GitHub <#2 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACGFS6L6T4HB2FELEFZMPKT35UISRAVCNFSM6AAAAAB5WEQK26VHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZTKNJVGMYDONBZG4> . You are receiving this because you were mentioned.Message ID: ***@***.***>