Skip to content
LeanAuto CI

Enable Boogie variables to be monotonic #277

Sign in to view logs

Enable Boogie variables to be monotonic

Enable Boogie variables to be monotonic #277

Triggered via pull request September 23, 2024 16:06
@keyboardDrummerkeyboardDrummer
synchronize #951
keyboardDrummer:monotonicVariables
Status Failure
Total duration 43s
Artifacts –

test-lean-auto.yml

on: pull_request
LeanAuto CI
30s
LeanAuto CI
Fit to window
Zoom out
Zoom in

Annotations

7 errors and 1 warning
LeanAuto CI: Source/Core/StandardVisitor.cs#L1398
Argument 1: cannot convert from 'System.Collections.Generic.IEnumerable<Microsoft.Boogie.IdentifierExpr>' to 'System.Collections.Generic.List<Microsoft.Boogie.IdentifierExpr>'
LeanAuto CI: Source/Core/StandardVisitor.cs#L526
Property or indexer 'HavocCmd.Vars' cannot be assigned to -- it is read only
LeanAuto CI: Source/Core/StandardVisitor.cs#L526
Argument 1: cannot convert from 'System.Collections.Generic.IEnumerable<Microsoft.Boogie.IdentifierExpr>' to 'System.Collections.Generic.List<Microsoft.Boogie.IdentifierExpr>'
LeanAuto CI: Source/Core/StandardVisitor.cs#L1398
Argument 1: cannot convert from 'System.Collections.Generic.IEnumerable<Microsoft.Boogie.IdentifierExpr>' to 'System.Collections.Generic.List<Microsoft.Boogie.IdentifierExpr>'
LeanAuto CI: Source/Core/StandardVisitor.cs#L526
Property or indexer 'HavocCmd.Vars' cannot be assigned to -- it is read only
LeanAuto CI: Source/Core/StandardVisitor.cs#L526
Argument 1: cannot convert from 'System.Collections.Generic.IEnumerable<Microsoft.Boogie.IdentifierExpr>' to 'System.Collections.Generic.List<Microsoft.Boogie.IdentifierExpr>'
LeanAuto CI
Process completed with exit code 1.
LeanAuto CI
The following actions use a deprecated Node.js version and will be forced to run on node20: actions/setup-dotnet@v3, actions/checkout@v3. For more info: https://github.blog/changelog/2024-03-07-github-actions-all-actions-will-run-on-node20-instead-of-node16-by-default/