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.

Sign up for GitHub

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

Jump to bottom

Fix #659 #660

Merged
merged 4 commits into from
Jul 5, 2023
Merged

Fix #659 #660

merged 4 commits into from
Jul 5, 2023

Conversation

ArquintL
Copy link
Member

@ArquintL ArquintL commented Jul 4, 2023

Fixes #659
Includes changes of #658

@ArquintL ArquintL linked an issue Jul 4, 2023 that may be closed by this pull request
Quantified Let Expressions in Encoding Unsoundness #659
Closed
@ArquintL ArquintL requested a review from Dspil July 5, 2023 12:52
@ArquintL
Copy link
Member Author

ArquintL commented Jul 5, 2023

bors merge

bors bot added a commit that referenced this pull request Jul 5, 2023
@bors @ArquintL
Merge #660
6d4e05c 
660: Fix #659 r=ArquintL a=ArquintL

Fixes #659
Includes changes of #658

Co-authored-by: Linard Arquint <[email protected]>
@bors
Copy link
Contributor

bors bot commented Jul 5, 2023

This PR was included in a batch that successfully built, but then failed to merge into master. It will not be retried.

Additional information:

Response status code: 422
{"message":"You're not authorized to push to this branch. Visit https://docs.github.com/articles/about-protected-branches/ for more information.","documentation_url":"https://docs.github.com/articles/about-protected-branches"}

@ArquintL ArquintL merged commit ff48d9c into master Jul 5, 2023
3 checks passed
@ArquintL ArquintL deleted the 659-quantified-let-expressions-in-encoding-unsoundness branch July 5, 2023 14:08
koflin added a commit to koflin/gobra that referenced this pull request Aug 18, 2023
@koflin
Squashed commit of the following:
63b26cf 
commit caca746
Author: Felix Wolf <[email protected]>
Date:   Thu Aug 17 13:38:33 2023 +0200

    Fix viperproject#668 (viperproject#669)

commit f21fe70
Author: viper-admin <[email protected]>
Date:   Wed Aug 2 19:46:32 2023 +0200

    Updates submodules (viperproject#667)

    Co-authored-by: ArquintL <[email protected]>

commit 3590b3c
Merge: 4a27390 04a7a2a
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 16:20:45 2023 +0200

    Merge pull request viperproject#665 from viperproject/avoid-printing-asts

    Avoiding accidental printing of ASTs

commit 04a7a2a
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 15:07:32 2023 +0200

    adapts  to avoid accidental printing of ASTs

commit 4a27390
Merge: 8f9bfa7 a132190
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 10:02:56 2023 +0200

    Merge pull request viperproject#634 from viperproject/parallel-type-checking

    Parallelizing Gobra

commit a132190
Merge: 716eeeb 4fc3cc9
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 09:23:38 2023 +0200

    Merges remote changes

commit 716eeeb
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 09:23:21 2023 +0200

    implements CR suggestions by Felix

commit 4fc3cc9
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 09:06:13 2023 +0200

    Update src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

    Co-authored-by: Felix Wolf <[email protected]>

commit 8f9bfa7
Merge: 400015c 940a4b5
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 08:18:36 2023 +0200

    Merge pull request viperproject#664 from viperproject/auto-update-submodules

    Update Submodules

commit 940a4b5
Author: ArquintL <[email protected]>
Date:   Mon Jul 17 17:36:04 2023 +0000

    Updates submodules

commit 400015c
Merge: 1894cef 64389b2
Author: Linard Arquint <[email protected]>
Date:   Thu Jul 13 11:20:49 2023 +0200

    Merge pull request viperproject#663 from viperproject/auto-update-submodules

    Update Submodules

commit 64389b2
Author: ArquintL <[email protected]>
Date:   Thu Jul 13 07:54:42 2023 +0000

    Updates submodules

commit 1894cef
Author: viper-admin <[email protected]>
Date:   Wed Jul 12 06:56:11 2023 +0200

    Updates submodules (viperproject#661)

    Co-authored-by: jcp19 <[email protected]>

commit 6e21fcf
Merge: bb3610b ff48d9c
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 16:22:22 2023 +0200

    Merges branch 'master' into 'parallel-type-checking'

commit ff48d9c
Merge: c56b335 d34ca31
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 16:08:57 2023 +0200

    Merge pull request viperproject#660 from viperproject/659-quantified-let-expressions-in-encoding-unsoundness

    Fix viperproject#659

commit d34ca31
Merge: 1929662 c56b335
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 15:33:11 2023 +0200

    Merges branch 'master' into '659-quantified-let-expressions-in-encoding-unsoundness'

commit c56b335
Merge: 4393ad0 fc634a4
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 15:32:22 2023 +0200

    Merge pull request viperproject#658 from viperproject/auto-update-submodules

    Update Submodules

commit 1929662
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 4 09:30:59 2023 +0200

    updates ViperServer to latest commit

commit 3e87a6a
Merge: 0fdf73a fc634a4
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 4 08:58:25 2023 +0200

    Merges branch 'auto-update-submodules' into '659-quantified-let-expressions-in-encoding-unsoundness'

commit 0fdf73a
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 4 08:57:32 2023 +0200

    adds failing test case

commit fc634a4
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 12:19:32 2023 +0200

    fixes a compiler error caused by recent error reporting improvements

commit d64f56a
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 12:05:30 2023 +0200

    adapts regression tests to latest Viper changes

commit 9772277
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 12:03:33 2023 +0200

    improves reporting of consistency errors and errors resulting from applying Viper transformers

commit 08bfba3
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 09:48:45 2023 +0200

    adapts 'builtin' and 'stubs' packages to latest changes in Viper

commit bb3610b
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 09:02:29 2023 +0200

    fixes a typo

commit a18c450
Author: ArquintL <[email protected]>
Date:   Sat Jul 1 06:00:52 2023 +0000

    Updates submodules

commit 50f379c
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 16:47:10 2023 +0200

    fixes unit tests by making type-check caching specific to the config's choice of 32 or 64bit ints

commit 52317a4
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 15:48:17 2023 +0200

    fixes compilation errors

commit cda37bc
Merge: 7f32830 4393ad0
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 14:50:54 2023 +0200

    Merges branch 'master' into 'pre-parse-unit-tests'

commit 7f32830
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 14:43:24 2023 +0200

    cleanup

commit e97cbf5
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 11:22:00 2023 +0200

    pre-parses and pre-typeChecks Gobra tests

commit 6f41997
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 09:51:57 2023 +0200

    addresses several unit test errors

commit 8d24c01
Author: Linard Arquint <[email protected]>
Date:   Thu Jun 29 17:02:23 2023 +0200

    fixes compilation issue and undos parser caching for unit tests

commit 046fe54
Author: Linard Arquint <[email protected]>
Date:   Thu Jun 29 16:43:04 2023 +0200

    unifies job managers for parsing and type-checking and for the 3 modes

commit 4393ad0
Author: viper-admin <[email protected]>
Date:   Wed May 31 20:13:50 2023 +0200

    Updates submodules (viperproject#657)

    Co-authored-by: jcp19 <[email protected]>

commit ed3aaf4
Author: Felix Wolf <[email protected]>
Date:   Wed May 31 20:13:16 2023 +0200

    Fix viperproject#655 (viperproject#656)

    * Fix viperproject#655

    * fixed reintroduced bug

commit 5aa73b1
Author: viper-admin <[email protected]>
Date:   Fri May 19 15:45:09 2023 +0200

    Updates submodules (viperproject#654)

    Co-authored-by: jcp19 <[email protected]>

commit 5aeb8bf
Author: viper-admin <[email protected]>
Date:   Tue May 16 12:02:56 2023 +0200

    Updates submodules (viperproject#653)

    Co-authored-by: jcp19 <[email protected]>

commit 178f985
Author: João Pereira <[email protected]>
Date:   Sun May 14 17:35:44 2023 +0200

    Fix issue 651 (viperproject#652)

    * Add bug witness

    * Add fix

    * Reflect that the order of fields matter in the signature of AdtClauseT

    * use more general type

commit 3ce34f3
Author: viper-admin <[email protected]>
Date:   Fri May 12 16:59:46 2023 +0200

    Updates submodules (viperproject#650)

    Co-authored-by: jcp19 <[email protected]>

commit c0e1c40
Author: João Pereira <[email protected]>
Date:   Thu May 11 19:50:47 2023 +0200

    Update tutorial.md (viperproject#603)

commit f4babde
Author: viper-admin <[email protected]>
Date:   Fri May 5 18:38:26 2023 +0200

    Updates submodules (viperproject#648)

    Co-authored-by: jcp19 <[email protected]>

commit 686b53d
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 11:23:54 2023 +0100

    Parses all inputs to 'GobraTests' in parallel before actually starting the unit tests

commit c00c636
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 30 14:02:13 2023 +0200

    adds a sequential parser

commit cfed2ce
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 30 09:50:34 2023 +0200

    fixes reporting of errors in imported packages and reports them as part of type-checking

commit 169d091
Author: Linard Arquint <[email protected]>
Date:   Wed Mar 15 19:46:48 2023 +0100

    fixes parser error messages

commit ba5f161
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 17:59:26 2023 +0100

    cleans up

commit 3ed1598
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 17:36:43 2023 +0100

    fixes unit tests

commit 66f542d
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 08:56:09 2023 +0100

    Revert "restricts unit tests to 'regressions/features/header_only'"

    This reverts commit 53453f0.

commit 9edc26e
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 08:54:47 2023 +0100

    propagates parsing exceptions, built-in files are always considered even with  enabled

commit 53453f0
Author: Linard Arquint <[email protected]>
Date:   Mon Mar 13 14:21:29 2023 +0100

    restricts unit tests to 'regressions/features/header_only'

commit 04874c9
Author: Linard Arquint <[email protected]>
Date:   Fri Mar 10 16:02:12 2023 +0100

    fixes a unit test

commit a2b9b6c
Author: Linard Arquint <[email protected]>
Date:   Fri Mar 10 15:43:46 2023 +0100

    adds PPackage caching to parser

commit a45f58c
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 15:12:10 2023 +0100

    fixes license headers

commit db26519
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 15:10:54 2023 +0100

    fixes license headers

commit 5a4f353
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 15:07:44 2023 +0100

    fixes unit tests

commit 81ea403
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 09:38:03 2023 +0100

    saves ongoing work

commit 8039bcf
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 09:32:22 2023 +0100

    updates ANTLR Go lexer and parser

commit 62d6349
Author: Linard Arquint <[email protected]>
Date:   Sat Mar 4 20:22:55 2023 +0100

    saves on-going work
koflin added a commit to koflin/gobra that referenced this pull request Aug 18, 2023
@koflin
Squashed commit of the following:
948b641 
commit caca746
Author: Felix Wolf <[email protected]>
Date:   Thu Aug 17 13:38:33 2023 +0200

    Fix viperproject#668 (viperproject#669)

commit f21fe70
Author: viper-admin <[email protected]>
Date:   Wed Aug 2 19:46:32 2023 +0200

    Updates submodules (viperproject#667)

    Co-authored-by: ArquintL <[email protected]>

commit 3590b3c
Merge: 4a27390 04a7a2a
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 16:20:45 2023 +0200

    Merge pull request viperproject#665 from viperproject/avoid-printing-asts

    Avoiding accidental printing of ASTs

commit 04a7a2a
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 15:07:32 2023 +0200

    adapts  to avoid accidental printing of ASTs

commit 4a27390
Merge: 8f9bfa7 a132190
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 10:02:56 2023 +0200

    Merge pull request viperproject#634 from viperproject/parallel-type-checking

    Parallelizing Gobra

commit a132190
Merge: 716eeeb 4fc3cc9
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 09:23:38 2023 +0200

    Merges remote changes

commit 716eeeb
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 09:23:21 2023 +0200

    implements CR suggestions by Felix

commit 4fc3cc9
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 09:06:13 2023 +0200

    Update src/main/scala/viper/gobra/frontend/info/implementation/resolution/MemberResolution.scala

    Co-authored-by: Felix Wolf <[email protected]>

commit 8f9bfa7
Merge: 400015c 940a4b5
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 18 08:18:36 2023 +0200

    Merge pull request viperproject#664 from viperproject/auto-update-submodules

    Update Submodules

commit 940a4b5
Author: ArquintL <[email protected]>
Date:   Mon Jul 17 17:36:04 2023 +0000

    Updates submodules

commit 400015c
Merge: 1894cef 64389b2
Author: Linard Arquint <[email protected]>
Date:   Thu Jul 13 11:20:49 2023 +0200

    Merge pull request viperproject#663 from viperproject/auto-update-submodules

    Update Submodules

commit 64389b2
Author: ArquintL <[email protected]>
Date:   Thu Jul 13 07:54:42 2023 +0000

    Updates submodules

commit 1894cef
Author: viper-admin <[email protected]>
Date:   Wed Jul 12 06:56:11 2023 +0200

    Updates submodules (viperproject#661)

    Co-authored-by: jcp19 <[email protected]>

commit 6e21fcf
Merge: bb3610b ff48d9c
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 16:22:22 2023 +0200

    Merges branch 'master' into 'parallel-type-checking'

commit ff48d9c
Merge: c56b335 d34ca31
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 16:08:57 2023 +0200

    Merge pull request viperproject#660 from viperproject/659-quantified-let-expressions-in-encoding-unsoundness

    Fix viperproject#659

commit d34ca31
Merge: 1929662 c56b335
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 15:33:11 2023 +0200

    Merges branch 'master' into '659-quantified-let-expressions-in-encoding-unsoundness'

commit c56b335
Merge: 4393ad0 fc634a4
Author: Linard Arquint <[email protected]>
Date:   Wed Jul 5 15:32:22 2023 +0200

    Merge pull request viperproject#658 from viperproject/auto-update-submodules

    Update Submodules

commit 1929662
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 4 09:30:59 2023 +0200

    updates ViperServer to latest commit

commit 3e87a6a
Merge: 0fdf73a fc634a4
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 4 08:58:25 2023 +0200

    Merges branch 'auto-update-submodules' into '659-quantified-let-expressions-in-encoding-unsoundness'

commit 0fdf73a
Author: Linard Arquint <[email protected]>
Date:   Tue Jul 4 08:57:32 2023 +0200

    adds failing test case

commit fc634a4
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 12:19:32 2023 +0200

    fixes a compiler error caused by recent error reporting improvements

commit d64f56a
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 12:05:30 2023 +0200

    adapts regression tests to latest Viper changes

commit 9772277
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 12:03:33 2023 +0200

    improves reporting of consistency errors and errors resulting from applying Viper transformers

commit 08bfba3
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 09:48:45 2023 +0200

    adapts 'builtin' and 'stubs' packages to latest changes in Viper

commit bb3610b
Author: Linard Arquint <[email protected]>
Date:   Mon Jul 3 09:02:29 2023 +0200

    fixes a typo

commit a18c450
Author: ArquintL <[email protected]>
Date:   Sat Jul 1 06:00:52 2023 +0000

    Updates submodules

commit 50f379c
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 16:47:10 2023 +0200

    fixes unit tests by making type-check caching specific to the config's choice of 32 or 64bit ints

commit 52317a4
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 15:48:17 2023 +0200

    fixes compilation errors

commit cda37bc
Merge: 7f32830 4393ad0
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 14:50:54 2023 +0200

    Merges branch 'master' into 'pre-parse-unit-tests'

commit 7f32830
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 14:43:24 2023 +0200

    cleanup

commit e97cbf5
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 11:22:00 2023 +0200

    pre-parses and pre-typeChecks Gobra tests

commit 6f41997
Author: Linard Arquint <[email protected]>
Date:   Fri Jun 30 09:51:57 2023 +0200

    addresses several unit test errors

commit 8d24c01
Author: Linard Arquint <[email protected]>
Date:   Thu Jun 29 17:02:23 2023 +0200

    fixes compilation issue and undos parser caching for unit tests

commit 046fe54
Author: Linard Arquint <[email protected]>
Date:   Thu Jun 29 16:43:04 2023 +0200

    unifies job managers for parsing and type-checking and for the 3 modes

commit 4393ad0
Author: viper-admin <[email protected]>
Date:   Wed May 31 20:13:50 2023 +0200

    Updates submodules (viperproject#657)

    Co-authored-by: jcp19 <[email protected]>

commit ed3aaf4
Author: Felix Wolf <[email protected]>
Date:   Wed May 31 20:13:16 2023 +0200

    Fix viperproject#655 (viperproject#656)

    * Fix viperproject#655

    * fixed reintroduced bug

commit 5aa73b1
Author: viper-admin <[email protected]>
Date:   Fri May 19 15:45:09 2023 +0200

    Updates submodules (viperproject#654)

    Co-authored-by: jcp19 <[email protected]>

commit 5aeb8bf
Author: viper-admin <[email protected]>
Date:   Tue May 16 12:02:56 2023 +0200

    Updates submodules (viperproject#653)

    Co-authored-by: jcp19 <[email protected]>

commit 178f985
Author: João Pereira <[email protected]>
Date:   Sun May 14 17:35:44 2023 +0200

    Fix issue 651 (viperproject#652)

    * Add bug witness

    * Add fix

    * Reflect that the order of fields matter in the signature of AdtClauseT

    * use more general type

commit 3ce34f3
Author: viper-admin <[email protected]>
Date:   Fri May 12 16:59:46 2023 +0200

    Updates submodules (viperproject#650)

    Co-authored-by: jcp19 <[email protected]>

commit c0e1c40
Author: João Pereira <[email protected]>
Date:   Thu May 11 19:50:47 2023 +0200

    Update tutorial.md (viperproject#603)

commit f4babde
Author: viper-admin <[email protected]>
Date:   Fri May 5 18:38:26 2023 +0200

    Updates submodules (viperproject#648)

    Co-authored-by: jcp19 <[email protected]>

commit 686b53d
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 11:23:54 2023 +0100

    Parses all inputs to 'GobraTests' in parallel before actually starting the unit tests

commit c00c636
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 30 14:02:13 2023 +0200

    adds a sequential parser

commit cfed2ce
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 30 09:50:34 2023 +0200

    fixes reporting of errors in imported packages and reports them as part of type-checking

commit 169d091
Author: Linard Arquint <[email protected]>
Date:   Wed Mar 15 19:46:48 2023 +0100

    fixes parser error messages

commit ba5f161
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 17:59:26 2023 +0100

    cleans up

commit 3ed1598
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 17:36:43 2023 +0100

    fixes unit tests

commit 66f542d
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 08:56:09 2023 +0100

    Revert "restricts unit tests to 'regressions/features/header_only'"

    This reverts commit 53453f0.

commit 9edc26e
Author: Linard Arquint <[email protected]>
Date:   Tue Mar 14 08:54:47 2023 +0100

    propagates parsing exceptions, built-in files are always considered even with  enabled

commit 53453f0
Author: Linard Arquint <[email protected]>
Date:   Mon Mar 13 14:21:29 2023 +0100

    restricts unit tests to 'regressions/features/header_only'

commit 04874c9
Author: Linard Arquint <[email protected]>
Date:   Fri Mar 10 16:02:12 2023 +0100

    fixes a unit test

commit a2b9b6c
Author: Linard Arquint <[email protected]>
Date:   Fri Mar 10 15:43:46 2023 +0100

    adds PPackage caching to parser

commit a45f58c
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 15:12:10 2023 +0100

    fixes license headers

commit db26519
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 15:10:54 2023 +0100

    fixes license headers

commit 5a4f353
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 15:07:44 2023 +0100

    fixes unit tests

commit 81ea403
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 09:38:03 2023 +0100

    saves ongoing work

commit 8039bcf
Author: Linard Arquint <[email protected]>
Date:   Thu Mar 9 09:32:22 2023 +0100

    updates ANTLR Go lexer and parser

commit 62d6349
Author: Linard Arquint <[email protected]>
Date:   Sat Mar 4 20:22:55 2023 +0100

    saves on-going work
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Dspil Dspil Dspil approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

Quantified Let Expressions in Encoding Unsoundness
2 participants
@ArquintL @Dspil