The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option z3_with_extensions. Minor
INCOMPATIBILITY.
On 04.06.2012 09:28, Sascha Boehme wrote:
The SMT solver Z3 has now by default a restricted set of directly
supported features. For the full set of features (div/mod, nonlinear
arithmetic, datatypes/records) with potential proof reconstruction
failures, enable the configuration option
Hi Stefan,
while doing a testall on the AFP, I noticed that JinjaThreads no longer
compiles. I get the error
*** exception Match raised (line 146)
***
*** At command ML (line 145 of
/mnt/home/berghofe/isabelle/afp/thys/JinjaThreads/Examples/BufferExample.thy)
This should be now fixed in
