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

Examples: Theory Combination #451

Merged
merged 1 commit into from Dec 26, 2017

Conversation

Projects
None yet
2 participants
@marcogario
Contributor

marcogario commented Oct 22, 2017

Simple example using BV, Int, Real and Array.

@marcogario

This comment has been minimized.

Show comment
Hide comment
@marcogario

marcogario Oct 22, 2017

Contributor

This depends on #450

Contributor

marcogario commented Oct 22, 2017

This depends on #450

@marcogario marcogario added this to the 0.7.5 milestone Nov 18, 2017

@marcogario marcogario self-assigned this Nov 23, 2017

@marcogario marcogario assigned mikand and unassigned marcogario Dec 23, 2017

@mikand mikand merged commit 765d2ce into master Dec 26, 2017

5 checks passed

clahub All contributors have signed the Contributor License Agreement.
Details
continuous-integration/appveyor/branch AppVeyor build succeeded
Details
continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
continuous-integration/travis-ci/push The Travis CI build passed
Details

@mikand mikand deleted the i414/examples_theory_combination branch Dec 26, 2017

mikand added a commit that referenced this pull request Jan 2, 2018

Fixed typing error in msat back
The recently added theory combination example raised a typing error within the back function of the msat converter. The error was due to INT/REAL distinction made by pysmt that is ignored by mathsat for numeric constants. The fix consists in asking the type system of mathsat the relevant types instead of determining them using the pysmt type-checker.

NOTE: this bug was highlighted by the new "theory combination" example added in #451 but the PR was accepted beacuse Travis is currently broken. We need to finish with #469 to trust CI again.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment