Fix infinite loop in datatypes enumerator. Minor work on conjecture generator.
authorajreynol <andrew.j.reynolds@gmail.com>
Wed, 24 Sep 2014 14:42:31 +0000 (16:42 +0200)
committerajreynol <andrew.j.reynolds@gmail.com>
Wed, 24 Sep 2014 14:42:31 +0000 (16:42 +0200)
commitd38d41b3f3604fc728ec71499d1f3af3dfb46ccd
tree009798015a508c4f257c599d3aca810ea2540bf4
parent4d7329f72720e884a6161dcdeb8d377d19031930
Fix infinite loop in datatypes enumerator.  Minor work on conjecture generator.
src/theory/datatypes/type_enumerator.h
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/conjecture_generator.h
test/regress/regress0/datatypes/Makefile.am
test/regress/regress0/datatypes/tenum-bug.smt2 [new file with mode: 0644]