[Question][Hw6] Several questions

[sms0509]

1. I think that spec.param and spec.vars should contain exactly same variables since the function Spec.verify gives counterexamples for spec.param. So to test constraints with these examples, shouldn't they be same?

2. Is it possible that the verify function distinguishes the input parameters of target function? According to the code in language.ml I think this is impossible since "to_z3expr" function does not care about the parameters of functions. I even think that the "args" argument in "to_z3expr" has no meaning since this is never used.

3. Could you give me some hints about 'why the crash occurs'? I first think that this is the problem regarding to the parameters of functions in constraints, but this does not make sense according to the above two questions.

I'm asking these questions because I've spent a lot of time on this task, but I haven't made any progress.
There is a limit that I can solve with bottomup search and equivalence reduction. However, since there are many people who have solved this task, I think I am missing an important part of this task, so I want to know that part.

Thank you.

[Hhro]

1. Yeap, they should be same.
2. Yes, you are right. Based on our implementation, input parameters cannot be distinguished, and args are not used. I think there are some implementation mistakes; we should've defined the function declaration for f and applied it properly to the function call inside constraints. (@KihongHeo; Please take a look)
3. It is introduced after [Question][Hw6] Request for information in leaderboard #109.
   Precisely, we evaluate your synthesis according to the following rule:
   • Correct: Emit valid program within time budget (2min)
   • Timeout: Synthesis hasn't completed until the time's over
   • Crash: Every other cases (e.g. failwith, Z3 runtime error, e.t.c. )

[Lee-Janggun]

For me, I used my bottom-up code from homework 4 as-is, removed some optimizations that couldn't be applied to CEGIS or was buggy for some other reason, and added logic in dealing with counterexample returned by Spec.verify. To try out more examples for debugging, I used the examples in HW4, with the single constraint of (= (f x y) "whatever the expected function is").

[sms0509]

Thank you for your replies. I'll try it again.