about summary refs log tree commit diff homepage
path: root/lib
diff options
context:
space:
mode:
authorHristina Palikareva <h.palikareva@imperial.ac.uk>2013-10-10 12:23:20 +0100
committerHristina Palikareva <h.palikareva@imperial.ac.uk>2013-10-11 20:02:33 +0100
commitf53b2ebc74acd9d31b54f21434e1b21eed7f5787 (patch)
treee634015a9287be2cb832e5bf6d37b3a0d8ab2600 /lib
parentd508fcc715277ea0a22c007ecde6ebc991d81841 (diff)
downloadklee-f53b2ebc74acd9d31b54f21434e1b21eed7f5787.tar.gz
getConstraintLog() of MetaSMTSolver explicitly states that this feature is not supported; a test case modified to not fail because of this.
Diffstat (limited to 'lib')
-rw-r--r--lib/Solver/Solver.cpp5
1 files changed, 4 insertions, 1 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 4df691f2..22b1545f 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -935,7 +935,10 @@ MetaSMTSolverImpl<SolverContext>::~MetaSMTSolverImpl() {
 
 template<typename SolverContext>
 char *MetaSMTSolverImpl<SolverContext>::getConstraintLog(const Query&) {
-  // ToDo
+  const char* msg = "Not supported";
+  char *buf = new char[strlen(msg) + 1];
+  strcpy(buf, msg);
+  return(buf);
 }
 
 template<typename SolverContext>