Sankalp Gambhir
Sankalp Gambhir
Filed a dotty issue: https://github.com/lampepfl/dotty/issues/19031 Seems to be a problem with the way we declare an `InnerProof` inside `Proof` as extending it. Pattern match exhaustion checking seems to fail. Minimized...
I'm not sure if there is a good solution to this. Initialization of objects is generally out of our hands. We can (and did) use the compiler option to ensure...
Despite the closing of #120, this one continues to struggle (just tried).
Probably a bigger issue, is that these are not caught during proof construction to return an `InvalidProofTactic`, but rather throw (currently uncaught) exceptions.
Oh thanks, I was not in the loop on that! My bad for not checking the open PRs. I mostly wanted to leave this here so I have a documented...
Okay I have a (shady) fix for this. In `src/main/scala/inox/solvers/z3/NativeZ3Optimizer.scala`, change every instance of `targetProgram` to `aliased` and define: ```scala private val aliased: targetProgram.type = targetProgram ``` (the access permissions...
@dhalilov this PR is dependent on a PR on your fork, dhalilov/lisa#1 to handle some merge conflicts
Update: after #166, I will need to update dhalilov/lisa#1 as well to fix some conflicts
I think it's a good change! It would simplify testing Stainless and Inox together. With the current dependency setup, you often end up with sbt recompiling Inox entirely on any...
Thanks! I can confirm that this is rejected on the main branch.