diff options
| author | ajreynol <reynolds@larapc05.epfl.ch> | 2014-06-17 15:25:58 +0200 |
|---|---|---|
| committer | lianah <lianahady@gmail.com> | 2014-06-19 18:24:39 -0400 |
| commit | 0fe78eebc0c0f2d01c7aa64725bee08ba5aa2274 (patch) | |
| tree | 475b094989b0828d7d82e41160a010a6134e8674 /src/util/sort_inference.cpp | |
| parent | 35cdae503bd88633a52333bf06fbf80cd81926e2 (diff) | |
For casc : print models of functions rewritten by sort inference.
Diffstat (limited to 'src/util/sort_inference.cpp')
| -rw-r--r-- | src/util/sort_inference.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index b38ed7d63..90382c365 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -580,6 +580,8 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ ss << "io_" << op; TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; + d_model_replace_f[op] = d_symbol_map[op]; }else{ d_symbol_map[op] = op; } |