diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-03-24 17:44:52 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-24 22:44:52 +0000 |
| commit | 77b75a69e51b742e1448d754b6886c10ef76e79f (patch) | |
| tree | b3c4f9793fc0db34494e1d914286e32a1bd4c04c /src/theory/quantifiers/fmf/model_engine.cpp | |
| parent | cfe207563479a1e9e13d52bdd93446a8c816636a (diff) | |
Use inference manager to access intantiate utility instead of quantifiers engine (#6198)
Towards breaking dependencies on quantifers engine.
Diffstat (limited to 'src/theory/quantifiers/fmf/model_engine.cpp')
| -rw-r--r-- | src/theory/quantifiers/fmf/model_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/fmf/model_engine.cpp b/src/theory/quantifiers/fmf/model_engine.cpp index eb7398f92..b05f25b5e 100644 --- a/src/theory/quantifiers/fmf/model_engine.cpp +++ b/src/theory/quantifiers/fmf/model_engine.cpp @@ -279,7 +279,7 @@ void ModelEngine::exhaustiveInstantiate( Node f, int effort ){ if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; - Instantiate* inst = d_quantEngine->getInstantiate(); + Instantiate* inst = d_qim.getInstantiate(); while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); |