mirror of
https://github.com/Z3Prover/z3
synced 2025-04-23 17:15:31 +00:00
make sure ackermann works with arrays that have more than one argument
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a3739aa934
commit
94d3c591b5
2 changed files with 2000 additions and 2100 deletions
|
@ -30,7 +30,10 @@ async function invokeLLMUpdate(code, inputFile) {
|
|||
let userMessage = `Please modify the original code to ensure that it enforces the following:
|
||||
- do not use pointer arithmetic.
|
||||
- do not introduce uses of std::vector.
|
||||
- only make replacements that are compatible with the ones listed below.
|
||||
- do not remove comments from the code.
|
||||
- do not replace for loops over unsigned by for loops over 'auto'.
|
||||
- keep comments in the same place. Please.
|
||||
- only make replacements that are compatible with the ones listed next:
|
||||
- add white space between operators:
|
||||
For example:
|
||||
i=0
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue