Bug fix for define functions + incremental. Minor work on relational triggers.
authorajreynol <andrew.j.reynolds@gmail.com>
Tue, 22 Mar 2016 19:07:21 +0000 (14:07 -0500)
committerajreynol <andrew.j.reynolds@gmail.com>
Tue, 22 Mar 2016 19:07:28 +0000 (14:07 -0500)
commit0ee7aa783c299eca1127005b590dd157b315f130
tree23d95924956b6bdcfc9a7bc9b6996ac00657007e
parent5d600cd2df87f81ec19034a79e7fe4eea9482b4c
Bug fix for define functions + incremental. Minor work on relational triggers.
src/smt/smt_engine.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
test/regress/regress0/push-pop/Makefile.am
test/regress/regress0/push-pop/inc-define.smt2 [new file with mode: 0644]