Mondok Milán
Mondok Milán
To the `Could not parse solver output: (error "Array theory solver does not yet support write-chains connecting two different constant arrays")` error of `cvc5:1.0.8`: https://github.com/cvc5/cvc5/issues/3065 We should try with a...
`cvc5:1.0.8`: A dummy assertion has to be added to A in case of interpolation
`mathsat:5.6.10`: Arrays with bools as key or value type are simply not supported. ``` (declare-fun _arr$0_0 () (Array Int Bool)) (error "Arrays with Bool as argument are not supported") ```
`cvc5` `1.1.0` and `1.0.9`: It seems that `pop` does not remove `declare-fun`-s. The following doesn't work with `1.0.9` and `1.1.0`, but works with newer or older versions: ``` (set-option :produce-models...
`SmtLibSolverTest` and `SmtLibItpSolverTest` work on Windows (after removing the OS assertions). The uninstall after the tests fails because it lacks permissions to delete the installed solver.
`princess:2023-06-19`: the HashMap had to be replaced with an IdentityHashMap, like in the case of SmtInterpol.
I think this would be challenging to introduce to Theta, because in a Theta choice statement, assumptions can appear in arbitrary places (inside very complicated control structures), not just the...
Great idea, I approve
> Extra info: > > * `--version` shows "no such option", > * while `CEGAR --version` actually shows `CEGAR version 6.8.6` - where I'm not sure if CEGAR means anything..?...