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

Counterexamples As Assumptions #5013

Merged
merged 86 commits into from
Apr 9, 2024
Merged
Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
86 commits
Select commit Hold shift + click to select a range
00b7477
Store Progress
Sep 4, 2023
cc874dc
minor changes
Oct 25, 2023
1be2388
Counterexample parity for extension vs command line
Nov 16, 2023
d5505f4
Update DafnyRef and dev/news
Nov 16, 2023
8d428bc
Update ProverLogRegression
Nov 16, 2023
77c4e8f
Update existing test
Nov 16, 2023
6683cc7
primitive types
Dec 2, 2023
94db77a
Merge branch 'CounterexampleParity' into CounterexamplesAsPredicates
Dec 2, 2023
8c87dff
Save temp changes
Dec 7, 2023
f38b9f1
Sync with master
Dec 10, 2023
f358e51
Add Values field
Dec 10, 2023
d3e50ec
Calculate Cardinality
Dec 10, 2023
038395a
Separate constraints into their own class
Dec 13, 2023
5cbe1de
Fixes and testing
Dec 14, 2023
acf2179
Resolve all literals
Dec 17, 2023
af19151
push minor fixes
Dec 19, 2023
0e7da20
Prevent inifinite recursion
Dec 19, 2023
b57b5f1
Keep track of MapEmpty
Dec 20, 2023
726c164
Fix arities
Dec 20, 2023
b8426f0
Modify definition selection
Dec 20, 2023
4ae99f6
Another small fix
Dec 20, 2023
1e2e991
Fix test
Dec 20, 2023
b4eb8a9
Update wellformedness rules
Dec 30, 2023
0284161
Change order of definitions
Dec 30, 2023
d021fa2
Pass Test Generation tests
Jan 12, 2024
fe7d9aa
Do not constrain elements of a sequence that are out of bounds
Jan 16, 2024
83cc425
Merge remote-tracking branch 'origin/master' into CounterexampleParity
Jan 19, 2024
d182a13
Enable counterexamples for multiple locations in the program
Jan 19, 2024
65d2c04
Temprorarily add boogie submodule
Jan 19, 2024
00fa2a5
Fix test-generation translation pass and Update tests
Jan 19, 2024
0d7789f
Fix variable printing order and update tests
Jan 19, 2024
d510eaa
Merge branch 'CounterexampleParity' into CounterexamplesAsPredicates
Jan 19, 2024
d5ea6e3
Remove accidentally committed fiels
Jan 19, 2024
b180b1e
Updated tests
Jan 22, 2024
8aa183b
Revert "Temprorarily add boogie submodule"
Jan 22, 2024
10002e4
Update Boogie version
Jan 22, 2024
76700d7
Fix customBoogie.patchj
Jan 22, 2024
37bf3aa
Merge branch 'master' into CounterexampleParity
Jan 22, 2024
8515c8e
Update Prover Log test
Jan 22, 2024
c06d769
Update Inverses test
Jan 22, 2024
3f2eb86
Merge branch 'CounterexampleParity' into CounterexamplesAsPredicates
Jan 22, 2024
fdaa5c6
Pass all server tests
Jan 25, 2024
ab0ec83
Merge remote-tracking branch 'origin/master' into CounterexamplesAsPr…
Jan 25, 2024
c72299d
Remove unused code
Jan 25, 2024
7e7f0f8
Format and test output fies
Jan 25, 2024
b111ba2
Fix tests
Dargones Feb 1, 2024
43436e2
Refactor the constraints mechanism
Feb 9, 2024
a19dc32
Refactor Constraint.cs
Feb 10, 2024
dce077d
Minor fixes
Feb 10, 2024
4f71e2c
Fix an inconsistent counterexample
Feb 11, 2024
61e5b9a
Merge remote-tracking branch 'origin/master' into CounterexamplesAsPr…
Feb 11, 2024
ca31a49
Fix whitespace
Feb 11, 2024
931e0df
Fix Arity
Feb 11, 2024
7042d0e
Deal with Empty Sequences
Feb 11, 2024
42c62b3
Handle collection types with no argument
Feb 11, 2024
c58a225
Support constraints over function return values
Feb 19, 2024
581d51f
Generate on test method at a time
Feb 19, 2024
bfcb31e
Fix wellformedness checks
Feb 19, 2024
4c14080
Merge remote-tracking branch 'origin/CounterexamplesAsPredicates' int…
Feb 19, 2024
9d7e2c8
Better Documentation and formatting
Feb 22, 2024
7b85179
Dotnet format
Feb 22, 2024
80c3838
Delete accidentally committed files
Feb 22, 2024
7de5b4a
Fix tests
Feb 22, 2024
6f98747
Merge branch 'CounterexamplesAsPredicates' into CounterexamplesDev
Feb 25, 2024
70d516e
Minor fixes
Feb 25, 2024
0bec799
Add SetDisplay Constraint
Feb 25, 2024
548e79b
Minor fix
Feb 25, 2024
c85769f
More fixes
Feb 25, 2024
5319003
Undo the tuple ignoring principle
Feb 25, 2024
32f7be5
Merge recent changes
Mar 7, 2024
699f52e
Merge remote-tracking branch 'origin/master' into CounterexamplesAsPr…
Mar 7, 2024
9c111f8
Apply suggested changes
Mar 7, 2024
36cd8d2
Update Source/DafnyLanguageServer/CounterExampleGeneration/DafnyModel.cs
Dargones Mar 7, 2024
40cabcf
Fix counterexample for recursive functions
Mar 7, 2024
a5149a9
Pretty-printing changes
Mar 13, 2024
e38dbc1
Fix tests
Mar 13, 2024
2e6415a
Merge remote-tracking branch 'origin/master' into CounterexamplesAsPr…
Mar 13, 2024
53904c3
Fix test
Mar 13, 2024
5975ea7
Add a warning indicating that the counterexample may be inconsistent …
Mar 21, 2024
6f36f77
Merge remote-tracking branch 'origin/master' into CounterexamplesAsPr…
Apr 8, 2024
203f725
Fix nitpick
Apr 8, 2024
48812d5
Lift note on counterexample validity into its own section
Apr 8, 2024
275db10
Fix tests
Apr 8, 2024
d964f3c
Merge branch 'master' into CounterexamplesAsPredicates
atomb Apr 9, 2024
fac4c7c
Merge branch 'master' into CounterexamplesAsPredicates
atomb Apr 9, 2024
a58755c
Merge branch 'master' into CounterexamplesAsPredicates
Dargones Apr 9, 2024
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
Update existing test
  • Loading branch information
Aleksandr Fedchin committed Nov 16, 2023
commit 77c4e8fb17c7501a174e756821a897d77a9b9096
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
// RUN: %exits-with 4 %dafny /compile:0 "%s" /extractCounterexample /mv model > "%t"
// RUN: %exits-with 4 %dafny /compile:0 /extractCounterexample "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

// NB: with recent Z3 versions (e.g., 4.12.1), this program no longer
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -3,30 +3,5 @@ git-issue-2026.dfy(18,18): Related message: loop invariant violation

Dafny program verifier finished with 0 verified, 1 error
Counterexample for first failing assertion:
git-issue-2026.dfy(12,0): initial state:
n : int = 2
ret : _System.array<seq<char>> = ()
git-issue-2026.dfy(13,24):
n : int = 2
ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
@0 : seq<char> = ['o', 'd', 'd']
git-issue-2026.dfy(15,14):
n : int = 2
ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
i : int = 0
@0 : seq<char> = ['o', 'd', 'd']
git-issue-2026.dfy(16,4): after some loop iterations:
n : int = 2
ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0)
i : int = 0
@0 : seq<char> = ['o', 'd', 'd']
git-issue-2026.dfy(22,27):
n : int = 2
ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
i : int = 0
@0 : seq<char> = ['o', 'd', 'd']
git-issue-2026.dfy(26,18):
n : int = 2
ret : _System.array?<seq<char>> = (Length := 2, [(- 7720)] := @0, [0] := @0)
i : int = 1
@0 : seq<char> = ['o', 'd', 'd']
Loading