diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-21 16:34:56 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-21 16:35:53 +0200 |
| commit | 82f4d5bd67f70a561b0f6357f6d6b80c2fcd7b64 (patch) | |
| tree | c55a17ef87f4a68a9a0de115fde101452d771dc7 /src/theory | |
| parent | 494bf99194fa4c9eb55eaffa0d090777a34e6359 (diff) | |
Fix bug in fmf mbqi=fmc with arrays. Add two datatypes regressions.
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/full_model_check.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 3148901da..5be263254 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -903,6 +903,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl; //uninterpreted compose doUninterpretedCompose( fm, f, d, n.getOperator(), children ); + /* } else if( n.getKind()==SELECT ){ Trace("fmc-debug") << "Do select compose " << n << std::endl; std::vector< Def > children2; @@ -911,6 +912,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n mkCondDefaultVec(fm, f, cond); std::vector< Node > val; doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val ); + */ } else { if( !var_ch.empty() ){ if( n.getKind()==EQUAL ){ |