We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
The following fails (on SMTLIB2Interface):
module main { datatype adt_t = A (i : integer, b : bv4) | B (i : integer, b : boolean); var adt1 : adt_t; var adt2 : adt_t; init { adt1 = B(10, true); adt2 = A(10, 4bv4); } next { adt1' = B(adt1.i+1, adt1.b); adt2' = A(adt2.i+1, adt2.b); } property match: adt1.i == adt2.i; control { v = bmc(2); check; print_results; v.print_cex_json(); } }
with
Type error at line 16: Argument type error in application. adt1' = B(adt1.i+1, adt1.b); ^ Parsing failed. 1 errors found.
Renaming apart the fields in the ADT to, e.g.,
datatype adt_t = A (ia : integer, ba : bv4) | B (ib : integer, bb : boolean);
fixes the issue.
Will explicitly forbidding field reuse across constructors fix this in general? If so, we could internally/silently perform field renaming.
Even if there is no change, we need some documentation clarifying such details.
The text was updated successfully, but these errors were encountered:
Added a new test tracking this: test-adt-28-fieldreuse.ucl
test-adt-28-fieldreuse.ucl
Sorry, something went wrong.
No branches or pull requests
The following fails (on SMTLIB2Interface):
with
Renaming apart the fields in the ADT to, e.g.,
fixes the issue.
Will explicitly forbidding field reuse across constructors fix this in general? If so, we could internally/silently perform field renaming.
Even if there is no change, we need some documentation clarifying such details.
The text was updated successfully, but these errors were encountered: