ths-rwth/smtrat

Issues

• Bug: Solver crashes on optimization problem

  #112 opened 3 months ago by bruderj15
  2

• cmake fails on MacOS 12.6.2 with Homebrew

  #109 opened 2 years ago by rpgoldman
  5

• Building in Dockerfile works but needs environment variable

  #110 opened 2 years ago by rpgoldman
  4

• --preprocess option no longer supported?

  #111 opened 2 years ago by rpgoldman
  2

• Have model that seems to parse successfully but hangs in preprocessing

  #108 opened 2 years ago by rpgoldman
  7

• Remove unnecessary null pointer checks

  #107 opened 2 years ago by elfring
  0

• Question about CoCOALib build in SMT-RAT

  #104 opened 2 years ago by rpgoldman
  1

• Request: Add installation instructions

  #100 opened 2 years ago by rpgoldman
  1

• Fix link on the homepage of this repo

  #103 opened 2 years ago by rpgoldman
  0

• Carl version mismatch? SMT-RAT build fails on Linux

  #105 opened 2 years ago by rpgoldman
  8

• Compilation fails because of use of gtest (googletest) test library

  #106 opened 2 years ago by rpgoldman
  2

• Quantifier Elimination Bug

  #95 opened 2 years ago by lalaniket8
  2

• Broken link to manual on home page

  #98 opened 2 years ago by rpgoldman
  1

• can build, but cannot install smtrat (CArL-EP-doxygen build step failure)

  #96 opened 2 years ago by maychiew1988
  4

• Unable to build on Linux: can't find carl header file

  #102 opened 2 years ago by rpgoldman
  4

• Request: Add example model files

  #101 opened 2 years ago by rpgoldman
  1

• Problem building on top of Carl

  #97 opened 2 years ago by rpgoldman
  4

• Syntax specification?

  #99 opened 2 years ago by rpgoldman
  2

• Suggestion for improvement

  #94 opened 3 years ago by dxliuNJU
  0

• Build failure

  #93 opened 4 years ago by abol-karimi
  1

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:3137 (mcsat)

  #92 opened 4 years ago by rainoftime
  0

• Segment fault on QF_LRA formula at carl/formula/Formula.h:283 (mcsat)

  #90 opened 4 years ago by rainoftime
  0

• Soundness bug on QF_NRA formula (mcsat)

  #91 opened 4 years ago by rainoftime
  0

• Assertion violation at smtrat-mcsat/assignments/arithmetic/../../utils/Bookkeeping.h:69

  #88 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-modules/SATModule/mcsat/MCSATMixin.tpp:170

  #89 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-modules/SATModule/mcsat/VarSchedulerMcsat.h:55(mcsat)

  #73 opened 4 years ago by rainoftime
  0

• Assertion violation at smtrat-modules/SATModule/mcsat/VarSchedulerMcsat.h:91(mcsat, incomplete fix)

  #87 opened 4 years ago by rainoftime
  0

• Assertion violation at CArL-EP/src/carl-model/ModelValue.h:210 (qe)

  #82 opened 4 years ago by rainoftime
  0

• Assertion violation at CArL-EP/src/carl/core/polynomialfunctions/RootFinder.tpp:35 (qe)

  #86 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:389 (mcsat)

  #71 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-modules/SATModule/mcsat/MCSATMixin.h:254 (mcsat)

  #74 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:1385 (mcsat)

  #75 opened 4 years ago by rainoftime
  1

• Assertion violation at CArL-EP/src/carl/core/polynomialfunctions/FieldExtensions.h:163 (mcsat)

  #76 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-mcsat/explanations/vs/ExplanationGenerator.h:110 (mcsat)

  #77 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-mcsat/explanations/vs/ExplanationGenerator.h:136 (mcsat)

  #78 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-mcsat/explanations/onecellcad/OneCellCAD.h:969 (mcsat)

  #79 opened 4 years ago by rainoftime
  1

• Soundness issue on QF_NIA formula (mcsat)

  #80 opened 4 years ago by rainoftime
  1

• Assertion violation at smtrat-modules/SATModule/mcsat/VarSchedulerMcsat.h:91(mcsat)

  #72 opened 5 years ago by rainoftime
  1

• Assertion violation at smtrat-qe/cad/Projection.h:53 (qe)

  #81 opened 5 years ago by rainoftime
  1

• Segment fault at UnivariatePolynomial.h:156

  #63 opened 5 years ago by rainoftime
  2

• Assertion violation at cli/tools/ExecutionState.h:132

  #67 opened 5 years ago by rainoftime
  2

• Assertion violation at cli/tools/ExecutionState.h:194

  #68 opened 5 years ago by rainoftime
  1

• Assertion violation at lib/datastructures/VariableBounds.tpp:535 (qe)

  #85 opened 5 years ago by rainoftime
  0

• Assertion violation at lib/datastructures/VariableBounds.h:168 (qe)

  #84 opened 5 years ago by rainoftime
  0

• Assertion violation at smtrat-cad/utils/CADConstraints.h:131 (qe)

  #83 opened 5 years ago by rainoftime
  0

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:3104 (--print-all-models)

  #69 opened 5 years ago by rainoftime
  0

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:770 (--print-all-models)

  #64 opened 5 years ago by rainoftime
  0

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:813 (--print-all-models)

  #66 opened 5 years ago by rainoftime
  0

• Assertion violation at smtrat-modules/IncWidthModule/IncWidthModule.cpp:167

  #70 opened 5 years ago by rainoftime
  0

• Assertion violation at smtrat-modules/SATModule/SATModule.cpp:3439 (--print-all-models)

  #65 opened 5 years ago by rainoftime
  0