about summary refs log tree commit diff homepage
path: root/lib/Solver
AgeCommit message (Expand)Author
2015-12-04Remove dead ``tempVars`` and ``getTempVar()`` method in STPBuilderDan Liew
2015-09-22[STPBuilder] Generate SRrem expressions correctlyMartin Nowack
2015-09-21Merge pull request #274 from MartinNowack/fix_sdiv_1Cristian Cadar
2015-09-05Allow to generate initial values with empty constraint setMartin Nowack
2015-08-30Fix signed division by constant 1/ -1Martin Nowack
2015-08-03Merge pull request #198 from holycrap872/IndependentSolverGetInitialValuesCristian Cadar
2015-07-06Make the super-set check in CexCachingSolver default offEric Rizzi
2015-04-01Added the function IndependentSolver::createdPointEvaluatesToTrueEric Rizzi
2015-04-01Commit of improved IndependentSolver::getIniitalValues().Eric Rizzi
2015-04-01Added the ability to solve for all factors in a particular query.Eric Rizzi
2015-03-20[Solver] Fix leak intermediate expression not freedMartin Nowack
2015-03-10Altered DenseSet and IndependentElementSet to record ref<Expr> involvedEric Rizzi
2014-12-09Merge pull request #186 from paulmar/fixshiftCristian Cadar
2014-12-08Fix overshift checkPaul Marinescu
2014-12-03Handling overshift behaviour in MetaSMTBuilderHristina Palikareva
2014-12-02Implement :named and let abbreviation modes in ExprSMTLIBPrinterRaimondas Sasnauskas
2014-09-14Fix compilation error due to change in raw_fd_ostream for LLVM3.5Dan Liew
2014-09-13[Solver] Tune down the shared memory region size on Darwin.Daniel Dunbar
2014-09-13[Solver] Ensure shared memory allocation failures are reported as errors, not...Daniel Dunbar
2014-09-13Add KLEE specific DEBUG macros.Daniel Dunbar
2014-09-12When building against libc++ (vs libstdcxx), use standard unordered_{map,set}...Daniel Dunbar
2014-05-29Use LLVM DEBUG macro instead of #if 0 or #if DEBUGMartin Nowack
2014-05-29Remove #include <iostream> to avoid static constructorsMartin Nowack
2014-05-29Refactoring from std::ostream to llvm::raw_ostreamMartin Nowack
2014-04-24Fixed order of domain and range in array creation in MetaSMTBuilder.Hristina Palikareva
2014-04-24Fixed creation of arrays with variable domains and ranges in STPBuilder and M...Hristina Palikareva
2014-04-24Remove unused pointer to STPSolver in STPSolverImpl to silence clangDan Liew
2014-04-16Removing a few more hard-coded values for domains and ranges of Array objectsHristina Palikareva
2014-04-15Associate a domain and range with each arrayPeter Collingbourne
2014-02-14Explicitly get the width of the "shift" expression rather than assumingDan Liew
2014-02-14Remove STPBuilder::getShiftBits() which is no longer used.Dan Liew
2014-02-14Fixed overshift of arithmetic right shift by constant so that itDan Liew
2014-02-14Fixed overshift of arithmetic right shift by symbolic so that it overshiftsDan Liew
2014-02-14Fixed overshift of logical right shift by constant so that itDan Liew
2014-02-14Fixed overshift of logical right shift by symbolic so that it overshiftsDan Liew
2014-02-14Fixed overshifting an expression by a constant so that we overshift toDan Liew
2014-02-14Added a test case for testing overshift behaviour of Shl and fixedDan Liew
2014-02-14Translate shl overshifts into 0Paul Marinescu
2013-12-21Do not install KLEE's internal libraries.Dan Liew
2013-10-11getConstraintLog() of MetaSMTSolver explicitly states that this feature is no...Hristina Palikareva
2013-10-11Bug fix in MetaSMTBuilderHristina Palikareva
2013-10-11MetaSMT builder, solver and command-line options.Hristina Palikareva
2013-09-17Merge pull request #21 from delcypher/fix_query_loggingCristian Cadar
2013-08-28Fix constness warnings issued by gcc 4.7Martin Nowack
2013-08-23In QueryLoggingSolver call flush() on std::ofstream so that queriesDan Liew
2013-08-06Methods getConstraintLog() and setTimeout() made virtual and moved from STPSo...Hristina Palikareva
2013-08-06Renaming solver-related command-line options in order to decouple them from S...Hristina Palikareva
2013-07-11Fixed and improved the stats on (cex)cache hits and misses.Cristian Cadar
2013-01-22Added a new option --ignore-solver-failures, disabled by default, toCristian Cadar
2013-01-02Forgot to add QueryLoggingSolver in patch 171387 from Tomasz Kuchta.Cristian Cadar