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

339 stackoverflowerror using mathsat5 #345

Merged
merged 46 commits into from
Jan 3, 2024
Merged

339 stackoverflowerror using mathsat5 #345

merged 46 commits into from
Jan 3, 2024

Commits on Dec 8, 2023

  1. Added tests to narrow down bug #339. So far no luck, but we did stumb… 

    …le upon bug #310 for CVC5.
    @daniel-raffler
    daniel-raffler committed Dec 8, 2023
    Configuration menu
    Copy the full SHA
    02d93be View commit details
    Browse the repository at this point in the history

Commits on Dec 10, 2023

  1. Fix build issues.

    @daniel-raffler
    daniel-raffler committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    65e4c32 View commit details
    Browse the repository at this point in the history

  2. Fixed checkstyle errors.

    @daniel-raffler
    daniel-raffler committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    5e1f046 View commit details
    Browse the repository at this point in the history

  3. Fixed license header.

    @daniel-raffler
    daniel-raffler committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    fb3d922 View commit details
    Browse the repository at this point in the history

  4. Fixed nonlocalContext test in SolverThreadLocalTest.

    @daniel-raffler
    daniel-raffler committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    f02f9ad View commit details
    Browse the repository at this point in the history

  5. Fixed bug in nonlocalContext test.

    @daniel-raffler
    daniel-raffler committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    202722b View commit details
    Browse the repository at this point in the history

  6. Make sure new context gets closed in SolverThreadLocal.nonlocalContext.

    @daniel-raffler
    daniel-raffler committed Dec 10, 2023
    Configuration menu
    Copy the full SHA
    01c3ce4 View commit details
    Browse the repository at this point in the history

Commits on Dec 14, 2023

  1. Added assertion to check if ShutdownNotifer was actually triggered wh… 

    …en MathSat returns a "user-requested termination" error.
    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    4003c34 View commit details
    Browse the repository at this point in the history

  2. Suppress resource warnings when using Executors.newSingleThreadExecutor.

    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    6e356cb View commit details
    Browse the repository at this point in the history

  3. Rewrote termination check for MathSAT to address the failed assertion… 

    … from 4003c34.
    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    c8c7712 View commit details
    Browse the repository at this point in the history

  4. Fixed formating

    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    3196f7f View commit details
    Browse the repository at this point in the history

  5. Added tests for interpolation to SolverThreadLocalTest. This includes… 

    … a test for bug #339 in MathSAT.
    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    9e2abee View commit details
    Browse the repository at this point in the history

  6. Simplified nonLocalProverTest

    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    8871155 View commit details
    Browse the repository at this point in the history

  7. Added a minimal test case for bug #339.

    @daniel-raffler
    daniel-raffler committed Dec 14, 2023
    Configuration menu
    Copy the full SHA
    d78b8f4 View commit details
    Browse the repository at this point in the history

Commits on Dec 15, 2023

  1. Added a native version of the testcase for #339.

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    9197ed1 View commit details
    Browse the repository at this point in the history

  2. Fixed formating

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    74f4a25 View commit details
    Browse the repository at this point in the history

  3. Added another version of the native test for #339 that fixes the bug.

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    bd81f54 View commit details
    Browse the repository at this point in the history

  4. Bugfix for #339

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    4464c90 View commit details
    Browse the repository at this point in the history

  5. Revert "Rewrote termination check for MathSAT to address the failed a… 

    …ssertion from 4003c34."

This reverts commit c8c7712.
    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    7adc7be View commit details
    Browse the repository at this point in the history

  6. Revert "Added assertion to check if ShutdownNotifer was actually trig… 

    …gered when MathSat returns a "user-requested termination" error."

This reverts commit 4003c34.
    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    9162b20 View commit details
    Browse the repository at this point in the history

  7. Disabled failing tests for CVC5

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    c41df5c View commit details
    Browse the repository at this point in the history

  8. Added copyright header to Bug339Test.java

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    e7fda3d View commit details
    Browse the repository at this point in the history

  9. Fixed annotation for bug330BrokenTest: we expect this to fail

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    63f8a94 View commit details
    Browse the repository at this point in the history

  10. Applied refaster patch

    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    ea5b9e7 View commit details
    Browse the repository at this point in the history

  11. Progage InterruptedExceptionin Mathsat5AbstractProver.exec() to fix s… 

    …eceral failed tests in TimoutTest.java
    @daniel-raffler
    daniel-raffler committed Dec 15, 2023
    Configuration menu
    Copy the full SHA
    0436959 View commit details
    Browse the repository at this point in the history

Commits on Dec 19, 2023

  1. Cleaned up SolverThreadLocalTest class

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    dc5ee89 View commit details
    Browse the repository at this point in the history

  2. Renamed SolverThreadLocalTest class to SolverThreadLocalityTest

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    1e0319b View commit details
    Browse the repository at this point in the history

  3. Some clean-up

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    0b3c2b8 View commit details
    Browse the repository at this point in the history

  4. Added one more test to SolverThreadLocalityTest that checks what happ… 

    …eneds when formulas are used outside of their context.
    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    80ede24 View commit details
    Browse the repository at this point in the history

  5. Removed native API test for bug339 as it has been fixed.

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    36919ed View commit details
    Browse the repository at this point in the history

  6. Removed JavaSMT test class for bug339 as it has been fixed.

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    d1e85eb View commit details
    Browse the repository at this point in the history

  7. Removed unused imports.

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    389af9f View commit details
    Browse the repository at this point in the history

  8. Remove use of "synchornized" in Mathsat5AbstractProver. Mathsat only … 

    …support one thread per ProverEnvironment anyway.
    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    010ddc2 View commit details
    Browse the repository at this point in the history

  9. Remove use of "synchornized" in Mathsat5InterpolatingProver.

    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    a28e7cd View commit details
    Browse the repository at this point in the history

  10. Remove comment about bug #339 from SolverThreadLocalityTest as the is… 

    …sues has been solved.
    @daniel-raffler
    daniel-raffler committed Dec 19, 2023
    Configuration menu
    Copy the full SHA
    24d16e6 View commit details
    Browse the repository at this point in the history

Commits on Dec 20, 2023

  1. Fixed resource leak in SolverThreadLocalityTest. See #345 (comment)

    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    7b70824 View commit details
    Browse the repository at this point in the history

  2. Fixed a bug in SolverThreadLocalityTest.nonlocalInterpolationTest whe… 

    …re the test may fail if calculating interpolants took too long.
    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    7bde6ff View commit details
    Browse the repository at this point in the history

  3. SolverThreadLocalityTest: Moved hard problem generator global for all… 

    … tests.
    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    0fa64d4 View commit details
    Browse the repository at this point in the history

  4. SolverThreadLocalityTest: Don't catch InvalidConfigurationExceptions … 

    …when trying to create a new solver context. See #345 (comment)
    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    4246d86 View commit details
    Browse the repository at this point in the history

  5. MathSAT5AbstractProver: Remove the helper method exec and install the… 

    … termination test directly in isUnsat and isUnsatWithAssumptions. This was suggested in #345 (comment)
    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    57ca2f4 View commit details
    Browse the repository at this point in the history

  6. Fixed checkstyle warning

    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    c18121a View commit details
    Browse the repository at this point in the history

  7. Try and fix the AppVeyor issue.

    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    0f14370 View commit details
    Browse the repository at this point in the history

  8. Removed unnecessary "resource" annotations.

    @daniel-raffler
    daniel-raffler committed Dec 20, 2023
    Configuration menu
    Copy the full SHA
    151c2ed View commit details
    Browse the repository at this point in the history

Commits on Dec 26, 2023

  1. MathSAT: shorten some code and refactor callback-providing method. 

    This commit unifies the level of abstraction
for registering a shutdown-callback and removing the callback afterwards.
    @kfriedberger
    kfriedberger committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    9b1361c View commit details
    Browse the repository at this point in the history

  2. Test: improve and extend some documentation. 

    And fix a typo.
    @kfriedberger
    kfriedberger committed Dec 26, 2023
    Configuration menu
    Copy the full SHA
    85c6def View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2023

  1. Fixed nonLocalProverTest: To trigger this specific bug in CVC5 we nee… 

    …d to create the ProverEnvironment on the thread. The other version also fails, but for different reasons and this somehow got mixed up earlier.
    @daniel-raffler
    daniel-raffler committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    3ce7326 View commit details
    Browse the repository at this point in the history