Pierre Villemot
Pierre Villemot
Most of incorrect tests are about the old parser, so it is pointless to keep them since we don't plan to modify the parser soon and the parser will be...
In my opinion, the non-regression tests shouldn't fail in the normal situation. I agree to bring back challenges but I do think we should create a separate alias for them....
If some of them pass, we can put them in the non-regression folder. I don't use benchpress in the above script but we can add them on Marvin for instance.
> Because apparently if `e = A` then `e#bb` is unspecified (I didn't find much documentation on it). For example: > > ``` > type t = A | B...
If we put the challenge tests on Marvin, I think that we can remove them of the tests folder. I plan to add categories in Benchtop, so it will be...
Guillaume explained to me the meaning of the projector `n#i`. It's the dirty way to implement the ADT without pattern matching. The same trick is used in SMT lib. Since...
I put the successful challenges back. The failed ones will be tested on Marvin.
Is it ok for you?
You're right. It does return `unsat` only if we turn model generation on. Why we shouldn't support this before model generation? Is it too complicated with the current implementation and...
I agree, we can activate model generation by default, at least in presence of theory for which model generation extends their support as record and ADT theories. Not sure it's...