projects
/
cvc5.git
/ history
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
Fix warnings and enable -Wnon-virtual-dtor warning (#2079)
[cvc5.git]
/
test
/
2018-06-21
Andres Noetzli
Check unsat cores in regressions also without LFSC...
tree
|
commitdiff
2018-06-15
Andrew Reynolds
Disable solving non-linear BV literals by default ...
tree
|
commitdiff
2018-06-13
Andrew Reynolds
Fix simple regexp consume (#2066)
tree
|
commitdiff
2018-06-12
Andrew Reynolds
Fix strip constant endpoint for ITOS in strings rewrite...
tree
|
commitdiff
2018-06-11
Andrew Reynolds
Fix equality conflicts reported by FP (#2064)
tree
|
commitdiff
2018-06-10
Andres Noetzli
Disable test that fails in competition mode (#2063)
tree
|
commitdiff
2018-06-09
Andres Noetzli
Add flag to skip regression if feature enabled (#2062)
tree
|
commitdiff
2018-06-09
Andres Noetzli
Reset decisions at SAT level after solving (#2059)
tree
|
commitdiff
2018-06-05
Andres Noetzli
Only enable transcendentals if logic is N[I]RAT (#2052)
tree
|
commitdiff
2018-06-04
Andrew Reynolds
Enable cegqi (with model values) for floating point...
tree
|
commitdiff
2018-06-04
Andres Noetzli
Regressions: Support for requiring CVC4 features (...
tree
|
commitdiff
2018-06-02
Mathias Preiner
Fix BV-abstraction check to consider SKOLEM. (#2042)
tree
|
commitdiff
2018-06-02
Andrew Reynolds
Fix preinitialization pass for finite model finding...
tree
|
commitdiff
2018-06-01
Andrew Reynolds
Fix quantified bv variable elimination (#2039)
tree
|
commitdiff
2018-06-01
Andrew Reynolds
Apply preprocessing to counterexample lemmas in CEGQI...
tree
|
commitdiff
2018-06-01
Andrew Reynolds
Use monomial sum utility to solve for quantifiers...
tree
|
commitdiff
2018-05-31
Mathias Preiner
Fix bv-abstraction check for AND with non bit-vector...
tree
|
commitdiff
2018-05-29
Andres Noetzli
Make user's SMT2 version override file version (#2004)
tree
|
commitdiff
2018-05-25
Andrew Reynolds
Reenable repair const (#1983)
tree
|
commitdiff
2018-05-24
Andrew Reynolds
Fix nl regression for unsat cores. (#1973)
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Generalize check-model in NonLinearExtension for quadra...
tree
|
commitdiff
2018-05-23
Andres Noetzli
Set same options for proofs as for unsat cores (#1957)
tree
|
commitdiff
2018-05-23
Andrew Reynolds
Repair constants using symbolic constructors (#1960)
tree
|
commitdiff
2018-05-22
Andrew Reynolds
Make sygus infer find function definitions (#1951)
tree
|
commitdiff
2018-05-21
Andrew Reynolds
Improvements in parsing and printing related to mixed...
tree
|
commitdiff
2018-05-21
Andrew Reynolds
Infrastructure to mark unused sygus strategies (#1950)
tree
|
commitdiff
2018-05-21
makaimann
Handle IMPLIES in bool-to-bv and test it in regress0...
tree
|
commitdiff
2018-05-21
Caleb Donovick
Fix file extension (#1919)
tree
|
commitdiff
2018-05-18
Andrew Reynolds
Cegis unif defaults to cegis when no unif (#1942)
tree
|
commitdiff
2018-05-18
Andrew Reynolds
Unified fairness scheme for cegis unif (#1941)
tree
|
commitdiff
2018-05-17
Andrew Reynolds
Fix debugPrint and add regress. (#1934)
tree
|
commitdiff
2018-05-17
Andrew Reynolds
Cegis-specific infrastructure (#1933)
tree
|
commitdiff
2018-05-15
Haniel Barbosa
adding regressions (#1925)
tree
|
commitdiff
2018-05-15
Andrew Reynolds
Fix annotations in regress2. (#1917)
tree
|
commitdiff
2018-05-14
Andrew Reynolds
Add regressions, change defaults. (#1911)
tree
|
commitdiff
2018-05-14
Andrew Reynolds
Flag to check invariance of entire values in sygus...
tree
|
commitdiff
2018-05-11
Aina Niemetz
Remove obsolete unit test for ackermannization. (#1906)
tree
|
commitdiff
2018-05-11
Aina Niemetz
Fix ackermannize preprocessing pass. (#1904)
tree
|
commitdiff
2018-05-11
Andres Noetzli
Support multiple sets of command line args in regs...
tree
|
commitdiff
2018-05-10
Andrew Reynolds
Sygus repair constants (#1812)
tree
|
commitdiff
2018-05-09
Andrew Reynolds
Make symmetry-breaker-exp into a preprocessing pass...
tree
|
commitdiff
2018-05-08
Mathias Preiner
Refactor bv-abstraction preprocessing pass. (#1860)
tree
|
commitdiff
2018-05-08
Andrew Reynolds
Support for str.<= and str.< (#1882)
tree
|
commitdiff
2018-05-07
Andrew Reynolds
Add support for str.code (#1821)
tree
|
commitdiff
2018-05-04
Mathias Preiner
Refactor bv-intro-pow2 preprocessing pass. (#1851)
tree
|
commitdiff
2018-05-04
Andrew Reynolds
Sets subtypes (#1095)
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Interleave quantifiers checks with ground theory checks...
tree
|
commitdiff
2018-05-03
Andrew Reynolds
Initial support for string standard in smt lib 2.6...
tree
|
commitdiff
2018-05-01
Andrew Reynolds
Improve tangent planes for transcendental functions...
tree
|
commitdiff
2018-04-30
Haniel Barbosa
Refactor real2int (#1813)
tree
|
commitdiff
2018-04-30
Andres Noetzli
Disable unsat-cores/proofs for slow regression (#1835)
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Allow multiple functions in sygus unif approaches ...
tree
|
commitdiff
2018-04-30
Andrew Reynolds
Make factoring inference more aggressive (#1825)
tree
|
commitdiff
2018-04-25
yoni206
Refactor bv-to-bool and bool-to-bv preprocessing passes...
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Add benchmark requiring subgoal generation with inducti...
tree
|
commitdiff
2018-04-25
Andrew Reynolds
Fix issue with multi-triggers that include variable...
tree
|
commitdiff
2018-04-20
yoni206
Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv...
tree
|
commitdiff
2018-04-20
yoni206
Allow metadata lines in test files to have leading...
tree
|
commitdiff
2018-04-20
PaulMeng
Symmetry detection module (#1749)
tree
|
commitdiff
2018-04-20
Andres Noetzli
Restrict test summary to first-level subfolders (#1797)
tree
|
commitdiff
2018-04-19
Andres Noetzli
Refactor pbRewrites preprocessing pass (#1767)
tree
|
commitdiff
2018-04-17
Andres Noetzli
Add timeout (option) to regression script (#1786)
tree
|
commitdiff
2018-04-17
Andres Noetzli
Disable slow regression test (#1787)
tree
|
commitdiff
2018-04-16
Andres Noetzli
Disable check proofs/unsat cores for two regs (#1785)
tree
|
commitdiff
2018-04-14
Andres Noetzli
[Reg] Make status/unsat-core detection more robust...
tree
|
commitdiff
2018-04-14
Andres Noetzli
Fix get-unsat-core detection in regression script ...
tree
|
commitdiff
2018-04-13
Andres Noetzli
Fix issue in regression script when proofs enabled...
tree
|
commitdiff
2018-04-13
Andrew Reynolds
Fix alpha equivalence for higher-order (#1769)
tree
|
commitdiff
2018-04-11
Aina Niemetz
Refactored BVGauss preprocessing pass. (#1766)
tree
|
commitdiff
2018-04-11
Andrew Reynolds
Properly implement function extensionality based on...
tree
|
commitdiff
2018-04-10
Andrew Reynolds
Fix hasSubterm calls for higher-order (#1760)
tree
|
commitdiff
2018-04-10
Andrew Reynolds
Fix higher-order term indexing. (#1754)
tree
|
commitdiff
2018-04-06
Arjun Viswanathan
Add define rec fun to cvc parser (#1738)
tree
|
commitdiff
2018-04-06
Andres Noetzli
Python regression script (#1662)
tree
|
commitdiff
2018-04-05
Andres Noetzli
Update README for regression tests (#1746)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Fix for corner case of higher-order matching (#1708)
tree
|
commitdiff
2018-04-04
Andrew Reynolds
Option to turn arbitrary input into sygus (#1704)
tree
|
commitdiff
2018-04-03
Andrew Reynolds
Use choice when expanding definitions for inverse trans...
tree
|
commitdiff
2018-04-02
Clark Barrett
Remove references to nyu (#1721)
tree
|
commitdiff
2018-04-02
Mathias Preiner
Reorganize bitblaster code. (#1695)
tree
|
commitdiff
2018-03-30
Andrew Reynolds
Disable regression (#1731)
tree
|
commitdiff
2018-03-27
Andres Noetzli
Better normalization of string concatenation (#1719)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Add support for filtering regressions with regex (...
tree
|
commitdiff
2018-03-26
Andres Noetzli
Add reasoning for inequalities in str rewriter (#1713)
tree
|
commitdiff
2018-03-26
Andres Noetzli
Rewrites for substr of strings of length one (#1712)
tree
|
commitdiff
2018-03-23
Andrew Reynolds
Add a few quantifiers regressions to improve coverage...
tree
|
commitdiff
2018-03-21
Andres Noetzli
Fix 'make regress' (#1683)
tree
|
commitdiff
2018-03-21
Mathias Preiner
Refactor mkoptions (#1631)
tree
|
commitdiff
2018-03-21
Andres Noetzli
Move regression tests to single Makefile.am (#1658)
tree
|
commitdiff
2018-03-21
Andres Noetzli
Fix various regression tests (#1657)
tree
|
commitdiff
2018-03-21
Andrew Reynolds
Fix for string disequality processing (#1679)
tree
|
commitdiff
2018-03-20
Andrew Reynolds
Internally remove redundant assertions and infer equali...
tree
|
commitdiff
2018-03-20
Andrew Reynolds
Fix datatype dump regression. (#1672)
tree
|
commitdiff
2018-03-20
Andrew Reynolds
Enable CEGQI for non-linear (#1674)
tree
|
commitdiff
2018-03-09
Aina Niemetz
Add support for SMT-LIB v2.5 command get-unsat-assumpti...
tree
|
commitdiff
2018-03-09
Andres Noetzli
Skip (get-unsat-assumptions) tests not supported (...
tree
|
commitdiff
2018-03-09
Mathias Preiner
Fix Travis for unit test compilation errors. (#1651)
tree
|
commitdiff
2018-03-06
Andres Noetzli
Remove printf from output utilities (#1629)
tree
|
commitdiff
2018-03-06
Andrew Reynolds
Update semantics for string indexof and replace (#1630)
tree
|
commitdiff
2018-03-05
Aina Niemetz
Add support for check-sat-assuming. (#1637)
tree
|
commitdiff
next