diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-12-14 13:35:53 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-12-14 13:35:53 -0600 |
| commit | e16ab44a2b4622bb5745633cbafd43a0023a518c (patch) | |
| tree | d980bdc3dc771abfc8101036d1e2aaebc8020134 /src/theory/theory_model_builder.cpp | |
| parent | ad34df900d79aad64558b354a866870715bfd007 (diff) | |
| parent | effb0d47ba5bfaebae17dcd06153489dccd90eff (diff) | |
Merge branch 'master' into cav22-stringscav22-strings
Diffstat (limited to 'src/theory/theory_model_builder.cpp')
| -rw-r--r-- | src/theory/theory_model_builder.cpp | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index bc63aef97..a83527004 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -1034,7 +1034,7 @@ bool TheoryEngineModelBuilder::buildModel(TheoryModel* tm) if (!repSet.empty()) { Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() - << ", first = " << *(repSet.begin()) << endl; + << ", repSet = " << repSet << endl; Assert(false); } } @@ -1278,7 +1278,8 @@ void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) } std::stringstream ss; ss << "_arg_"; - Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues); + Rewriter* r = condenseFuncValues ? d_env.getRewriter() : nullptr; + Node val = ufmt.getFunctionValue(ss.str(), r); m->assignFunctionDefinition(f, val); // ufmt.debugPrint( std::cout, m ); } |