Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Fix: have test generation return sequences with elements of right type (
#5611) ### Description Fixes #5608 <!-- Is this a user-visible change? Remember to update RELEASE_NOTES.md --> <!-- Is this a bug fix for an issue visible in the latest release? Mention this in the PR details and ensure a patch release is considered --> ### How has this been tested? Passes the existing tests and fixes the issue: ``` import M method {:test} Test0() { var seqreal0 : seq<real> := [(1236 as real), (2437 as real)]; expect |seqreal0| >= 2, "If this check fails at runtime, the test does not meet the preconditions"; var r0 := M.example(seqreal0); } method {:test} Test1() { var seqreal0 : seq<real> := [-1.0, 0.0]; expect |seqreal0| >= 2, "If this check fails at runtime, the test does not meet the preconditions"; var r0 := M.example(seqreal0); } method {:test} Test2() { var seqreal0 : seq<real> := [0.0, 0.0]; expect |seqreal0| >= 2, "If this check fails at runtime, the test does not meet the preconditions"; var r0 := M.example(seqreal0); } } ``` <!-- Tests can be added to `Source/IntegrationTests/TestFiles/LitTests/LitTest/` or to `Source/*.Test/…` and run with `dotnet test` --> <small>By submitting this pull request, I confirm that my contribution is made under the terms of the [MIT license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>
- Loading branch information