summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2014-11-20Disable constants sharing in eq engine, disable hack in theory engine. ↵ajreynol
Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring. Fix assertion failure in quantifiers engine.
2014-11-18Compute model basis only for fmf. Add another co-datatype regression.ajreynol
2014-11-18Add local theory extensions instantiation strategy (incomplete). Refactor ↵ajreynol
how default options are set for quantifiers. Minor improvement to datatypes. Add unsat co-datatype regression. Clean up instantiation engine. Set inst level 0 on introduced constants for types with no ground terms. Return introduced constant for variable trigger when no ground terms exist.
2014-11-17Resource-limiting work.Liana Hadarean
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2014-11-10Bug 593 fix: if the type is finite, it is now considered for detecting ↵Dejan Jovanović
theories of nested terms.
2014-11-09Merge branch '1.4.x'Morgan Deters
2014-11-09Increase stack size when running regressions (fixes some regression crashes ↵Morgan Deters
on Mac).
2014-11-09Fix dt shared terms issue, reenable regression.ajreynol
2014-11-08Fix bug with incremental+datatypes. Minor cleanup. Disable regression ↵ajreynol
bug484, enable parsing_ringer.
2014-11-07Merge branch '1.4.x'Morgan Deters
Conflicts: src/smt/model_postprocessor.cpp test/regress/regress0/Makefile.am
2014-11-07Fix missing case in Boolean terms rewriting. (Resolves bug #596.)Morgan Deters
2014-11-07Merge branch '1.4.x'Morgan Deters
Conflicts: src/smt/model_postprocessor.cpp
2014-11-07Corrected fix for missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.
2014-11-07Revert "Fix missing case in model postprocessor (resolves bug #595)."Morgan Deters
This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a. Conflicts: test/regress/regress0/Makefile.am
2014-11-07Merge branch '1.4.x'Morgan Deters
Conflicts: test/regress/regress0/Makefile.am
2014-11-07Fix missing case in model postprocessor (resolves bug #595).Morgan Deters
2014-11-07Properly distinguish which EQC to assign values in datatypes, use ↵ajreynol
assertRepresentative. Disable regression related to records. Enable fmf-fun related regression (modified). Apply modified version of Morgan's patch to fix tuples/records in model. Fix bug with sort inference + patterns. Minor infrastructure.
2014-11-06Reenable regression. Add (for now, disabled) changes to datatypes theory ↵ajreynol
combination. Relax communication of dt facts.
2014-11-05More work on datatypes theory combination: fix bug in care graph, do not ↵ajreynol
assign values for EQC of datatype type that contain only terms belonging to other theories, do not treat APPLY_UF as congruence operator, communicate equalities involving terms of external kind. Minor fixes for fun_def_process. Other minor changes.
2014-11-01Fix bug 592: introduce skolem for dt instantiate lemma (avoids terms in ↵ajreynol
lemmas being rewritten). Minor improvement to dt care graph. Reenable regressions.
2014-11-01Fix some mistakes in datatypes theory combination, disable two regressions. ↵ajreynol
Minor fix for fun defs.
2014-10-31Do not allow duplication of function definitions. Set incomplete flag in ↵ajreynol
model builder.
2014-10-23Parsing and infrastructure support for SMT-LIBv2.5 input and output languages.Morgan Deters
* support for new commands meta-info, declare-const, echo, get-model, reset, and reset-assertions * support for set-option :global-declarations * support for set-option :produce-assertions * support for set-option :reproducible-resource-limit * support for get-info :assertion-stack-levels * support for set-info :smt-lib-version 2.5 * ascribe types for abstract values (the new 2.5 standard clarifies that this is required) * SMT-LIB v2.5 string literals (we still support 2.0 string literals when in 2.0 mode) What's still to do: * check-sat-assumptions/get-unsat-assumptions (still being hotly debated). Also set-option :produce-unsat-assumptions. * define-fun-rec doesn't allow mutual recursion * All options should be restored to defaults with (reset) command. (Currently :incremental and maybe others get "stuck" due to late driver integration.)
2014-10-22Fix bug590 regression distcheck failure from last night.Morgan Deters
2014-10-21Fixed bug 590, added regression testClark Barrett
2014-10-17Merge branch '1.4.x'Morgan Deters
2014-10-17Remove a bad (unstable, timing-dependent) test.Morgan Deters
2014-10-14Context-dependent expr attributes are now attached to a specific SmtEngine, ↵Morgan Deters
and the SAT context is owned by the SmtEngine.
2014-10-10Merge remote-tracking branch 'origin/1.4.x'Kshitij Bansal
2014-10-10Fix issue with shared but non-preregistered term setup. Thanks Alvise ↵Kshitij Bansal
Rabitti for the report.
2014-10-06Fix unit test that was broken with last commit.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06Fix a bug in tuple-record handling. Thanks to Saumya Debray for the report.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
2014-10-06fix for bug586Kshitij Bansal
2014-10-06Extended parsing testcase, with constant arrays and RESET.Morgan Deters
2014-10-06Merge branch '1.4.x'Morgan Deters
Conflicts: test/regress/regress0/arrays/Makefile.am
2014-10-06Fix native language parsing of chained-store expressions (resolves bug 585). ↵Morgan Deters
Thanks to Eric Seidel for the report. Also fixed some operator precedence problems w.r.t. store expressions and arithmetic.
2014-10-04Enable some old bug testcases that (maybe?) never got added.Morgan Deters
2014-10-03Add some (so far trivial) regressions for constant arrays.Morgan Deters
2014-10-03Merge branch '1.4.x'Morgan Deters
2014-10-03Fix unit test for ArrayStoreAll.Morgan Deters
2014-09-25fix unit test for new fair datatype enumerationMorgan Deters
2014-09-24Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.ajreynol
2014-09-17Fix soundness bug for quantifier macros involving Int/Real.ajreynol
2014-09-03Implement and enable --dt-var-exp-quant, cleanup trace messages, minor ↵ajreynol
changes for relevant term filtering.
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-28fixing bug580 caused by bad bv inequality explanationlianah
2014-08-22Unit test fix.Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback