equal
deleted
inserted
replaced
41 - The 'smt_oracle' option is now necessary when using the 'smt' method |
41 - The 'smt_oracle' option is now necessary when using the 'smt' method |
42 with a solver other than Z3. INCOMPATIBILITY. |
42 with a solver other than Z3. INCOMPATIBILITY. |
43 - The encoding to first-order logic is now more complete in the presence of |
43 - The encoding to first-order logic is now more complete in the presence of |
44 higher-order quantifiers. An 'smt_explicit_application' option has been |
44 higher-order quantifiers. An 'smt_explicit_application' option has been |
45 added to control this. INCOMPATIBILITY. |
45 added to control this. INCOMPATIBILITY. |
|
46 |
|
47 * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash |
|
48 with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY. |
46 |
49 |
47 |
50 |
48 *** System *** |
51 *** System *** |
49 |
52 |
50 * Windows and Cygwin is for x86_64 only. Old 32bit platform support has |
53 * Windows and Cygwin is for x86_64 only. Old 32bit platform support has |