Pierre Villemot
Pierre Villemot
I plan to use logs actually but for a later release. I agree to rename options and deprecated the older ones.
https://github.com/sneeuwballen/benchpress/blob/2d84e9d2d46637c6e85989ad3710a8edb7e76787/src/core/Run_proc.ml#L9-L41 Does `Ptime_clock.now ()` return the elapsed time? As an experimentation, I will replace `Ptime_clock.now ()` by `Sys.time` which returns the cpu time. It should fix my issue. If it...
I am trying another solution given by a colleague ;)
I'm doing a second pass on this PR. Sorry for the partial review.
In my opinion there are two issues here: 1. The fact that a polymorphic constant like `id` can flood the SAT solver with useless monomorphization of itself isn't a desired...
> for instance we should probably do some sort of round-robin strategy on the triggers we use for a given axiom, to ensure all triggers ultimately have a chance to...
> I think its worth adding a test with `forall _: x. forall _: y. exist ...` to make sure that the behavior is correct in this case as well....
The new fix has been tested. We got +19-0. I believe that we lost these tests with Dolmen only. I did a mistake in the previous patch because I thought...
I agree. We should clarify what is supposed to be a top level formula in Alt-Ergo. I think we should test this PR on psmt2 files.
To clarify the meaning of `top level` in `Alt-Ergo`, I wrote a better commentary: ``` Determine if the quantified formula is at the top level of an asserted formula. An...