diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-01 17:06:33 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-11-01 17:06:33 -0500 |
| commit | c547bd591891ffd9211ed3859b0a67423a708f25 (patch) | |
| tree | b6a046cdc9cc474102640067fe1d9d67a012ae25 /src/theory/theory_model_builder.cpp | |
| parent | 86c541cdf83e0b98def5a479d1da966f2e959408 (diff) | |
Fix non-termination in datatype type enumerator (#3369)
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index b1171f152..47355aa81 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -306,6 +306,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) return false; } + Trace("model-builder") + << "TheoryEngineModelBuilder: Preprocess build model..." << std::endl; // model-builder specific initialization if (!preProcessBuildModel(tm)) { @@ -315,6 +317,8 @@ bool TheoryEngineModelBuilder::buildModel(Model* m) return false; } + Trace("model-builder") + << "TheoryEngineModelBuilder: Add assignable subterms..." << std::endl; // Loop through all terms and make sure that assignable sub-terms are in the // equality engine // Also, record #eqc per type (for finite model finding) |