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

Replace z3 jar files with KSMT dependency #1941

Merged
merged 5 commits into from
Mar 15, 2023
Merged

Conversation

CaelmBleidd
Copy link
Member

@CaelmBleidd CaelmBleidd commented Mar 13, 2023

Replace prebuilt Z3 jars with KSMT dependency

Description

I've replaced prebuilt Z3 jars with KSMT dependency. It has three consequences:

  1. We no longer have to hold jar along with our source code in our repository and build it by hand
  2. We have an updated version of Z3 since KSMT 0.4.3 works with Z3 4.11.2. Because of that, we have to generalize Z3 expressions with types
  3. Now we have support for Apple Silicon processors

How to test

Automated tests

Since it is a global change, all automatic tests are affected by it.

Manual tests

It was tested with automatic tests on the pipeline on Ubuntu, locally on Windows and Mac with both M1 Pro and Intel-based processors.

Self-check list

  • I've set the proper labels for my PR (at least, for category and component).
  • PR title and description are clear and intelligible.
  • I've added enough comments to my code, particularly in hard-to-understand areas.
  • The functionality I've repaired, changed or added is covered with automated tests.
  • Manual tests have been provided optionally.
  • The documentation for the functionality I've been working on is up-to-date.

@CaelmBleidd CaelmBleidd added ctg-enhancement New feature, improvement or change request comp-symbolic-engine Issue is related to the symbolic execution engine lang-java Issue is related to Java support labels Mar 13, 2023
Copy link
Collaborator

@Domonion Domonion left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

lgtm

Copy link
Member

@Damtev Damtev left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

LGTM

@CaelmBleidd CaelmBleidd merged commit 88927a9 into main Mar 15, 2023
@CaelmBleidd CaelmBleidd deleted the caelmbleidd/z3_version branch March 15, 2023 09:25
denis-fokin pushed a commit that referenced this pull request Mar 15, 2023
@CaelmBleidd CaelmBleidd restored the caelmbleidd/z3_version branch March 15, 2023 17:11
@CaelmBleidd CaelmBleidd deleted the caelmbleidd/z3_version branch March 22, 2023 10:28
@alisevych alisevych mentioned this pull request Apr 18, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
comp-symbolic-engine Issue is related to the symbolic execution engine ctg-enhancement New feature, improvement or change request lang-java Issue is related to Java support
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants