Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Update tests to work with Z3 4.12.1 #3400

Merged
merged 110 commits into from
Feb 28, 2023
Merged
Changes from 1 commit
Commits
Show all changes
110 commits
Select commit Hold shift + click to select a range
aec5aa0
Reorder output of several tests
atomb Jan 24, 2023
534a69f
Bump libraries submodule
atomb Jan 24, 2023
e461695
Update CI to use Z3 4.11.2
atomb Jan 24, 2023
da2ee9b
Roughly update some tests to work with Z3 4.11.2
atomb Jan 24, 2023
a23e889
Update Z3 download URLs
atomb Jan 24, 2023
27429e4
Remove errant newline
atomb Jan 24, 2023
f092846
Fix ordering in expected output of doc test
atomb Jan 25, 2023
03e3a13
Fix Z3 option used in test generation
atomb Jan 26, 2023
36417d9
Allow a few more tests to pass
atomb Jan 26, 2023
ded3d93
Speed up a test
atomb Jan 26, 2023
0eff6ce
Update expected output
atomb Jan 26, 2023
b7e6f51
Temporarily disable a few hard proofs
atomb Jan 26, 2023
f817274
Update SnapshotableTrees.dfy to be easier
atomb Jan 26, 2023
2547af7
Speed up BreadthFirstSearch
atomb Jan 26, 2023
b20ee60
Allow ACL2-extractor to go through
atomb Jan 26, 2023
1e82a0e
Reduce timeout likelihood for MutexLifetime-short
atomb Jan 26, 2023
7b72ca7
Simplify Z3 version check in language server
atomb Jan 27, 2023
6c6be0c
Adjust assertion order in language server test
atomb Jan 27, 2023
671697c
Upgrade to Z3 4.12.1
atomb Jan 27, 2023
e30100d
Update a test to skip a check no longer relevant
atomb Jan 27, 2023
f1176b0
Update test for different models with newer Z3
atomb Jan 28, 2023
e0d3134
Update order of error messages
atomb Jan 28, 2023
97f2e78
Fix previously-broken test update
atomb Jan 28, 2023
0d01cf7
Change what Dafny's expected to prove in one case
atomb Jan 28, 2023
4acf36a
Speed up a verification by splitting assertions
atomb Jan 28, 2023
b031987
Update download URL for Linux Z3 releases
atomb Jan 30, 2023
c6833a9
Update TestGeneration tests to be more permissive
atomb Jan 30, 2023
c2866ac
Avoid missing errors in BitvectorsMore
atomb Jan 31, 2023
17ca607
Speed up dafny2/SnapshotableTrees.dfy
atomb Jan 31, 2023
ca920f9
Attempt XUnit tests on ubuntu-22.04
atomb Jan 31, 2023
b612552
Update all ubuntu-20.04 to ubuntu-22.04
atomb Feb 1, 2023
0fd95ca
Get a few more tests passing with Z3 4.12.1
atomb Feb 2, 2023
c1a37e4
Split out test of all-literals axiom
atomb Feb 2, 2023
89b458b
Update fuel tests
atomb Feb 2, 2023
a5a9020
Bump libraries submodule
atomb Feb 6, 2023
a5935db
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 6, 2023
c2e978f
Update fuel tests -- TODO: needs careful thought!
atomb Feb 6, 2023
477c51e
Remove overly restrictive checks from test generation tests
atomb Feb 7, 2023
fdba438
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 9, 2023
dcea69b
Revert "Attempt XUnit tests on ubuntu-22.04"
atomb Feb 11, 2023
7230d01
Revert "Update all ubuntu-20.04 to ubuntu-22.04"
atomb Feb 11, 2023
2e8c1c7
Try Z3 4.12.2 nightly
atomb Feb 11, 2023
2e856a6
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 13, 2023
5fe892c
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 15, 2023
0be00ac
Add more debug output to language server tests
atomb Feb 15, 2023
91c8efe
Use nightly builds in Makefile, too
atomb Feb 16, 2023
c04ee95
Use `/errorLimit:0` to allow all errors through
atomb Feb 16, 2023
ba8c6d1
Enable the proof of a difficult postcondition
atomb Feb 16, 2023
011b21f
Apply suggestion from @Dargones
atomb Feb 16, 2023
178915d
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 16, 2023
64bb1d0
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 17, 2023
dd6a5ae
Use custom-built Z3 binaries
atomb Feb 17, 2023
5c5d349
Fix some Z3 setup typos
atomb Feb 17, 2023
06fb478
Fix some more Z3-related paths
atomb Feb 17, 2023
e2ecab6
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 20, 2023
5218862
Log memory use around verification in language server
atomb Feb 20, 2023
c082a01
Run language server tests with one thread
atomb Feb 20, 2023
deda3f8
More deterministic test of --error-limit
atomb Feb 20, 2023
809b1d1
Temporarily disable the two most expensive tests
atomb Feb 21, 2023
d0ae816
Revert "Temporarily disable the two most expensive tests"
atomb Feb 21, 2023
3a31c38
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 21, 2023
6a9f3ab
Install Z3 4.8.5 _and_ 4.12.1 in CI and packaging
atomb Feb 21, 2023
846de6d
Set %z3 correctly for lit-style tests
atomb Feb 21, 2023
70ff9c4
Try running language server tests with Z3 4.8.5
atomb Feb 21, 2023
7793799
Revert XUnit configuration to release builds
atomb Feb 21, 2023
6e159d1
Fix typo
atomb Feb 21, 2023
65a2516
Fix typo
atomb Feb 21, 2023
7442149
Typo
atomb Feb 22, 2023
d9169a3
Make xUnit test tolerate other Z3 processes
atomb Feb 22, 2023
d44704f
Fix Z3 move on non-Windows
atomb Feb 22, 2023
1f47358
Fix z3 version printing for release workflows
atomb Feb 22, 2023
4d61647
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 22, 2023
98c25f7
Hopefully get xUnit tests working with old setup
atomb Feb 22, 2023
4ca6e61
Fix merge conflict artifact
atomb Feb 23, 2023
355e811
Fix Z3 path
atomb Feb 23, 2023
68f7be8
Undo changes that broke resource use test
atomb Feb 23, 2023
6a114d0
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 23, 2023
228a769
Update build to use both Z3 4.8.5 and 4.12.1
atomb Feb 23, 2023
add1e96
Fix Z3 path typo
atomb Feb 23, 2023
32d9823
Use our builds of Z3 4.8.5 in xUnit tests
atomb Feb 23, 2023
feb2b24
Use macos-11, not macos-latest, in xUnit tests
atomb Feb 23, 2023
f2d6da7
Merge branch 'dual-solvers' into update-tests-z3-4.11.2
atomb Feb 23, 2023
cad7593
Remove merge conflict artifact
atomb Feb 23, 2023
61aaf9e
Undo temporary changes
atomb Feb 23, 2023
6745194
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 23, 2023
50ce749
Fix a couple of test outputs
atomb Feb 23, 2023
6f2b1b6
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 23, 2023
85d5783
Update xUnit tests to Z3 4.12.1
atomb Feb 23, 2023
1081126
Update test results
atomb Feb 23, 2023
50049f8
Get one more test to pass
atomb Feb 23, 2023
6c1b354
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 24, 2023
2daef3a
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 27, 2023
3d59924
Update expected output ordering for Fuel.dfy
atomb Feb 27, 2023
86060d4
Get dafny1/MoreInduction.dfy to pass
atomb Feb 27, 2023
b3b2be5
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 27, 2023
9ddc588
Merge remote-tracking branch 'upstream/master' into update-tests-z3-4…
atomb Feb 27, 2023
8d8e327
Fix expected output order for git-issue-2299.dfy
atomb Feb 27, 2023
f156ca3
Get dafny2/SnapshotableTrees.dfy to pass
atomb Feb 27, 2023
21c6c1a
Change test output order
atomb Feb 28, 2023
ef0923e
One more proof obligation in one case
atomb Feb 28, 2023
910c8d1
Revert "One more proof obligation in one case"
atomb Feb 28, 2023
6592175
Revert "Change test output order"
atomb Feb 28, 2023
0e91d79
One more failed proof in SnapshotableTrees
atomb Feb 28, 2023
66994cc
Get vstte2012/BreadthFirstSearch.dfy working
atomb Feb 28, 2023
259891f
Fix some test outputs
atomb Feb 28, 2023
ab38ecc
Merge remote-tracking branch 'upstream/main-4.0' into update-tests-z3…
atomb Feb 28, 2023
0133584
Resolve conflicts properly
atomb Feb 28, 2023
eae661b
Update mklink command
atomb Feb 28, 2023
fa8053d
Fix tests
atomb Feb 28, 2023
48451aa
Disable output checking of SnapshotableTrees.dfy
atomb Feb 28, 2023
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Remove merge conflict artifact
atomb committed Feb 23, 2023

Verified

This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
commit cad7593b49a0261fd67c184b5021995c5ba9f968
8 changes: 0 additions & 8 deletions Test/dafny2/SnapshotableTrees.dfy
Original file line number Diff line number Diff line change
@@ -489,11 +489,7 @@ module SnapTree {
var initialized: bool
var stack: List

<<<<<<< HEAD
predicate {:opaque} Valid()
=======
opaque predicate Valid()
>>>>>>> upstream/master
reads this, IterRepr, T
reads if T != null then T.Repr else {}
ensures Valid() ==> T != null && IterRepr !! T.Repr
@@ -514,11 +510,7 @@ module SnapTree {
// * for Cons(p, rest), fragment [p.data]+p.right.Contents
// In each case, R(wlist,n,C,Nodes) implies that the fragment wlist proper is a prefix of C[n..].
// Nodes is (an overapproximation of) the set of nodes read by R.
<<<<<<< HEAD
static predicate {:opaque} R(wlist: List, n: int, C: seq<int>, Nodes: set<object>)
=======
static opaque predicate R(wlist: List, n: int, C: seq<int>, Nodes: set<object>)
>>>>>>> upstream/master
reads Nodes
decreases wlist
{