Code

Update tests to work with Z3 4.12.1#3400

Code

Merged

atomb merged 110 commits intodafny-lang:main-4.0dafny-lang/dafny:main-4.0from atomb:update-tests-z3-4.11.2atomb/dafny:update-tests-z3-4.11.2Copy head branch name to clipboardFeb 28, 2023

+140-120

Commits

Commits on Jan 24, 2023

• Reorder output of several tests

  atomb

  committed
  aec5aa0

  Copy full SHA for aec5aa0

• Bump libraries submodule

  atomb

  committed
  534a69f

  Copy full SHA for 534a69f

• Update CI to use Z3 4.11.2

  atomb

  committed
  e461695

  Copy full SHA for e461695

• Roughly update some tests to work with Z3 4.11.2

  Show description for da2ee9b
  atomb

  committed
  da2ee9b

  Copy full SHA for da2ee9b

• Update Z3 download URLs

  atomb

  committed
  a23e889

  Copy full SHA for a23e889

• Remove errant newline

  atomb

  committed
  27429e4

  Copy full SHA for 27429e4

Commits on Jan 25, 2023

• Fix ordering in expected output of doc test

  atomb

  committed
  f092846

  Copy full SHA for f092846

Commits on Jan 26, 2023

• Fix Z3 option used in test generation

  Show description for 03e3a13
  atomb

  committed
  03e3a13

  Copy full SHA for 03e3a13

• Allow a few more tests to pass

  atomb

  committed
  36417d9

  Copy full SHA for 36417d9

• Speed up a test

  Show description for ded3d93
  atomb

  committed
  ded3d93

  Copy full SHA for ded3d93

• Update expected output

  atomb

  committed
  0eff6ce

  Copy full SHA for 0eff6ce

• Temporarily disable a few hard proofs

  atomb

  committed
  b7e6f51

  Copy full SHA for b7e6f51

• Update SnapshotableTrees.dfy to be easier

  Show description for f817274
  atomb

  committed
  f817274

  Copy full SHA for f817274

• Speed up BreadthFirstSearch

  atomb

  committed
  2547af7

  Copy full SHA for 2547af7

• Allow ACL2-extractor to go through

  Show description for b20ee60
  atomb

  committed
  b20ee60

  Copy full SHA for b20ee60

• Reduce timeout likelihood for MutexLifetime-short

  atomb

  committed
  1e82a0e

  Copy full SHA for 1e82a0e

Commits on Jan 27, 2023

• Simplify Z3 version check in language server

  atomb

  committed
  7b72ca7

  Copy full SHA for 7b72ca7

• Adjust assertion order in language server test

  atomb

  committed
  6c6be0c

  Copy full SHA for 6c6be0c

• Upgrade to Z3 4.12.1

  Show description for 671697c
  atomb

  committed
  671697c

  Copy full SHA for 671697c

• Update a test to skip a check no longer relevant

  Show description for e30100d
  atomb

  committed
  e30100d

  Copy full SHA for e30100d

Commits on Jan 28, 2023

• Update test for different models with newer Z3

  Show description for f1176b0
  atomb

  committed
  f1176b0

  Copy full SHA for f1176b0

• Update order of error messages

  atomb

  committed
  e0d3134

  Copy full SHA for e0d3134

• Fix previously-broken test update

  atomb

  committed
  97f2e78

  Copy full SHA for 97f2e78

• Change what Dafny's expected to prove in one case

  Show description for 0d01cf7
  atomb

  committed
  0d01cf7

  Copy full SHA for 0d01cf7

• Speed up a verification by splitting assertions

  atomb

  committed
  4acf36a

  Copy full SHA for 4acf36a

Commits on Jan 30, 2023

• Update download URL for Linux Z3 releases

  atomb

  committed
  b031987

  Copy full SHA for b031987

• Update TestGeneration tests to be more permissive

  Show description for c6833a9
  atomb

  committed
  c6833a9

  Copy full SHA for c6833a9

Commits on Jan 31, 2023

• Avoid missing errors in BitvectorsMore

  Show description for c2866ac
  atomb

  committed
  c2866ac

  Copy full SHA for c2866ac

• Speed up dafny2/SnapshotableTrees.dfy

  atomb

  committed
  17ca607

  Copy full SHA for 17ca607

• Attempt XUnit tests on ubuntu-22.04

  Show description for ca920f9
  atomb

  committed
  ca920f9

  Copy full SHA for ca920f9

Commits on Feb 1, 2023

• Update all ubuntu-20.04 to ubuntu-22.04

  atomb

  committed
  b612552

  Copy full SHA for b612552

Commits on Feb 2, 2023

• Get a few more tests passing with Z3 4.12.1

  atomb

  committed
  0fd95ca

  Copy full SHA for 0fd95ca

• Split out test of all-literals axiom

  atomb

  committed
  c1a37e4

  Copy full SHA for c1a37e4

• Update fuel tests

  Show description for 89b458b
  atomb

  committed
  89b458b

  Copy full SHA for 89b458b

Commits on Feb 6, 2023

• Bump libraries submodule

  atomb

  committed
  a5a9020

  Copy full SHA for a5a9020

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  a5935db

  Copy full SHA for a5935db

• Update fuel tests -- TODO: needs careful thought!

  Show description for c2e978f
  atomb

  committed
  c2e978f

  Copy full SHA for c2e978f

Commits on Feb 7, 2023

• Remove overly restrictive checks from test generation tests

  Show description for 477c51e
  atomb

  committed
  477c51e

  Copy full SHA for 477c51e

Commits on Feb 9, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  fdba438

  Copy full SHA for fdba438

Commits on Feb 11, 2023

• Revert "Attempt XUnit tests on ubuntu-22.04"

  Show description for dcea69b
  atomb

  committed
  dcea69b

  Copy full SHA for dcea69b

• Revert "Update all ubuntu-20.04 to ubuntu-22.04"

  Show description for 7230d01
  atomb

  committed
  7230d01

  Copy full SHA for 7230d01

• Try Z3 4.12.2 nightly

  atomb

  committed
  2e8c1c7

  Copy full SHA for 2e8c1c7

Commits on Feb 13, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  2e856a6

  Copy full SHA for 2e856a6

Commits on Feb 15, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  5fe892c

  Copy full SHA for 5fe892c

• Add more debug output to language server tests

  Show description for 0be00ac
  atomb

  committed
  0be00ac

  Copy full SHA for 0be00ac

Commits on Feb 16, 2023

• Use nightly builds in Makefile, too

  atomb

  committed
  91c8efe

  Copy full SHA for 91c8efe

• Use /errorLimit:0 to allow all errors through

  atomb

  committed
  c04ee95

  Copy full SHA for c04ee95

• Enable the proof of a difficult postcondition

  atomb

  committed
  ba8c6d1

  Copy full SHA for ba8c6d1

• Apply suggestion from @Dargones

  atomb

  committed
  011b21f

  Copy full SHA for 011b21f

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  178915d

  Copy full SHA for 178915d

Commits on Feb 17, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  64bb1d0

  Copy full SHA for 64bb1d0

• Use custom-built Z3 binaries

  atomb

  committed
  dd6a5ae

  Copy full SHA for dd6a5ae

• Fix some Z3 setup typos

  atomb

  committed
  5c5d349

  Copy full SHA for 5c5d349

• Fix some more Z3-related paths

  atomb

  committed
  06fb478

  Copy full SHA for 06fb478

Commits on Feb 20, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  e2ecab6

  Copy full SHA for e2ecab6

• Log memory use around verification in language server

  atomb

  committed
  5218862

  Copy full SHA for 5218862

• Run language server tests with one thread

  atomb

  committed
  c082a01

  Copy full SHA for c082a01

• More deterministic test of --error-limit

  atomb

  committed
  deda3f8

  Copy full SHA for deda3f8

Commits on Feb 21, 2023

• Temporarily disable the two most expensive tests

  atomb

  committed
  809b1d1

  Copy full SHA for 809b1d1

• Revert "Temporarily disable the two most expensive tests"

  Show description for d0ae816
  atomb

  committed
  d0ae816

  Copy full SHA for d0ae816

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  3a31c38

  Copy full SHA for 3a31c38

• Install Z3 4.8.5 _and_ 4.12.1 in CI and packaging

  Show description for 6a9f3ab
  atomb

  committed
  6a9f3ab

  Copy full SHA for 6a9f3ab

• Set %z3 correctly for lit-style tests

  atomb

  committed
  846de6d

  Copy full SHA for 846de6d

• Try running language server tests with Z3 4.8.5

  atomb

  committed
  70ff9c4

  Copy full SHA for 70ff9c4

• Revert XUnit configuration to release builds

  atomb

  committed
  7793799

  Copy full SHA for 7793799

• Fix typo

  atomb

  committed
  6e159d1

  Copy full SHA for 6e159d1

• Fix typo

  atomb

  committed
  65a2516

  Copy full SHA for 65a2516

Commits on Feb 22, 2023

• Typo

  atomb

  committed
  7442149

  Copy full SHA for 7442149

• Make xUnit test tolerate other Z3 processes

  atomb

  committed
  d9169a3

  Copy full SHA for d9169a3

• Fix Z3 move on non-Windows

  atomb

  committed
  d44704f

  Copy full SHA for d44704f

• Fix z3 version printing for release workflows

  atomb

  committed
  1f47358

  Copy full SHA for 1f47358

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  4d61647

  Copy full SHA for 4d61647

• Hopefully get xUnit tests working with old setup

  atomb

  committed
  98c25f7

  Copy full SHA for 98c25f7

Commits on Feb 23, 2023

• Fix merge conflict artifact

  atomb

  committed
  4ca6e61

  Copy full SHA for 4ca6e61

• Fix Z3 path

  atomb

  committed
  355e811

  Copy full SHA for 355e811

• Undo changes that broke resource use test

  atomb

  committed
  68f7be8

  Copy full SHA for 68f7be8

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  6a114d0

  Copy full SHA for 6a114d0

• Update build to use both Z3 4.8.5 and 4.12.1

  Show description for 228a769
  atomb

  committed
  228a769

  Copy full SHA for 228a769

• Fix Z3 path typo

  atomb

  committed
  add1e96

  Copy full SHA for add1e96

• Use our builds of Z3 4.8.5 in xUnit tests

  atomb

  committed
  32d9823

  Copy full SHA for 32d9823

• Use macos-11, not macos-latest, in xUnit tests

  atomb

  committed
  feb2b24

  Copy full SHA for feb2b24

• Merge branch 'dual-solvers' into update-tests-z3-4.11.2

  atomb

  committed
  f2d6da7

  Copy full SHA for f2d6da7

• Remove merge conflict artifact

  atomb

  committed
  cad7593

  Copy full SHA for cad7593

• Undo temporary changes

  atomb

  committed
  61aaf9e

  Copy full SHA for 61aaf9e

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  6745194

  Copy full SHA for 6745194

• Fix a couple of test outputs

  atomb

  committed
  50ce749

  Copy full SHA for 50ce749

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  6f2b1b6

  Copy full SHA for 6f2b1b6

• Update xUnit tests to Z3 4.12.1

  atomb

  committed
  85d5783

  Copy full SHA for 85d5783

• Update test results

  atomb

  committed
  1081126

  Copy full SHA for 1081126

• Get one more test to pass

  atomb

  committed
  50049f8

  Copy full SHA for 50049f8

Commits on Feb 24, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  6c1b354

  Copy full SHA for 6c1b354

Commits on Feb 27, 2023

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  2daef3a

  Copy full SHA for 2daef3a

• Update expected output ordering for Fuel.dfy

  atomb

  committed
  3d59924

  Copy full SHA for 3d59924

• Get dafny1/MoreInduction.dfy to pass

  atomb

  committed
  86060d4

  Copy full SHA for 86060d4

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  b3b2be5

  Copy full SHA for b3b2be5

• Merge remote-tracking branch 'upstream/master' into update-tests-z3-4.11.2

  atomb

  committed
  9ddc588

  Copy full SHA for 9ddc588

• Fix expected output order for git-issue-2299.dfy

  atomb

  committed
  8d8e327

  Copy full SHA for 8d8e327

• Get dafny2/SnapshotableTrees.dfy to pass

  atomb

  committed
  f156ca3

  Copy full SHA for f156ca3

Commits on Feb 28, 2023

• Change test output order

  atomb

  committed
  21c6c1a

  Copy full SHA for 21c6c1a

• One more proof obligation in one case

  atomb

  committed
  ef0923e

  Copy full SHA for ef0923e

• Revert "One more proof obligation in one case"

  Show description for 910c8d1
  atomb

  committed
  910c8d1

  Copy full SHA for 910c8d1

• Revert "Change test output order"

  Show description for 6592175
  atomb

  committed
  6592175

  Copy full SHA for 6592175

• One more failed proof in SnapshotableTrees

  Show description for 0e91d79
  atomb

  committed
  0e91d79

  Copy full SHA for 0e91d79

• Get vstte2012/BreadthFirstSearch.dfy working

  atomb

  committed
  66994cc

  Copy full SHA for 66994cc

• Fix some test outputs

  atomb

  committed
  259891f

  Copy full SHA for 259891f

• Merge remote-tracking branch 'upstream/main-4.0' into update-tests-z3-4.11.2

  atomb

  committed
  ab38ecc

  Copy full SHA for ab38ecc

• Resolve conflicts properly

  atomb

  committed
  0133584

  Copy full SHA for 0133584

• Update mklink command

  atomb

  committed
  eae661b

  Copy full SHA for eae661b

• Fix tests

  Show description for fa8053d
  atomb

  committed
  fa8053d

  Copy full SHA for fa8053d

• Disable output checking of SnapshotableTrees.dfy

  atomb

  committed
  48451aa

  Copy full SHA for 48451aa