diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 16:05:37 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-03 16:15:14 -0500 |
| commit | 72cae59d28aa43b734148090feb3b8cf4ecd2074 (patch) | |
| tree | 0a35cb1c706abfb5d6f37694779bbf895fd6b4d3 /src/smt/smt_engine.cpp | |
| parent | c7892fd17983a27d06b56c47f8125d50c691451c (diff) | |
Some cleanup of miplib regressions and options
Diffstat (limited to 'src/smt/smt_engine.cpp')
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 73e2b84c4..4104c0916 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2202,7 +2202,6 @@ void SmtEnginePrivate::doMiplibTrick() { Debug("miplib") << " -- INELIGIBLE " << (*j).first << " -- (insufficiently marked, got " << (*j).second << " for " << numVars << " vars, expected " << expected << endl; } else { if(false) { //checks[(*j).first] != coef[(*j).first][0] + coef[(*j).first][1]) { -#warning fixme Debug("miplib") << " -- INELIGIBLE " << (*j).first << " -- (not linear combination)" << endl; } else { Debug("miplib") << " -- ELIGIBLE " << *i << " , " << (*j).first << " --" << endl; @@ -2252,7 +2251,7 @@ void SmtEnginePrivate::doMiplibTrick() { //Warning() << "REPLACE " << newAssertion[1] << endl; //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl; Assert(d_topLevelSubstitutions.getSubstitution(newAssertion[0]) == newAssertion[1]); - } else if(arithMLTrickSubstitutions) { + } else if(options::arithMLTrickSubstitutions()) { d_topLevelSubstitutions.addSubstitution(newAssertion[0], newAssertion[1]); } Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl; |