Skip to content

Comments

[Bennet] Conditional lazy generation#497

Merged
ZippeyKeys12 merged 1 commit intorems-project:mainfrom
ZippeyKeys12:some-eager
Feb 3, 2026
Merged

[Bennet] Conditional lazy generation#497
ZippeyKeys12 merged 1 commit intorems-project:mainfrom
ZippeyKeys12:some-eager

Conversation

@ZippeyKeys12
Copy link
Collaborator

@ZippeyKeys12 ZippeyKeys12 commented Feb 3, 2026

This fixes lazy generation for tutorial_queue.pass.c

Suppose we have the following.

let* x = lazy<pointer>();
let* y = OtherGen(x);
let* z = ... ;
instantiate(x) { ... };
long x := z;

If x is instantiated in OtherGen, that point can not be backtracked to, from x := z.
Therefore, we now keep x's generation eager, resulting in:

let* x = arbitrary<pointer>();
let* y = OtherGen(x);
let* z = ... ;
long x := z;

@ZippeyKeys12 ZippeyKeys12 self-assigned this Feb 3, 2026
@ZippeyKeys12 ZippeyKeys12 added enhancement New feature or request Bennet Related to input generation via random backtracking search. Available via `cn test` labels Feb 3, 2026
@ZippeyKeys12 ZippeyKeys12 merged commit 0d56b2a into rems-project:main Feb 3, 2026
14 checks passed
@ZippeyKeys12 ZippeyKeys12 deleted the some-eager branch February 3, 2026 17:31
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Bennet Related to input generation via random backtracking search. Available via `cn test` enhancement New feature or request

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant