about summary refs log tree commit diff homepage
path: root/test
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-01-07 12:00:25 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2016-01-12 11:40:39 +0000
commite81f5ceed580d4d267e3c857b47637d6bd065499 (patch)
treeeb9f3b74b036a59edd1164bc68e9e00d5156936d /test
parent9da07ca0ccc58286f8247bc2e7d7745abfa0cc54 (diff)
downloadklee-e81f5ceed580d4d267e3c857b47637d6bd065499.tar.gz
Refactor setting the core solver (i.e. STP, MetaSMT or DummySolver) by providing
a ``createCoreSolver()`` function. The solver used is set by the new
``--solver-backend`` command line argument. The default is STP.

This change necessitated refactoring the MetaSMT stuff. That clearly
didn't belong in the Executor! The MetaSMT command line option is
now ``--metasmt-backend`` as this only picks the MetaSMT backend.

In order to use MetaSMT ``--solver-backend=metasmt`` needs to be passed.

Note I don't have MetaSMT built on my development machine so I don't
know if the MetaSMT stuff even compiles...
Diffstat (limited to 'test')
-rw-r--r--test/Solver/FastCexSolver.pc2
1 files changed, 1 insertions, 1 deletions
diff --git a/test/Solver/FastCexSolver.pc b/test/Solver/FastCexSolver.pc
index b8f839c3..b3ec63e3 100644
--- a/test/Solver/FastCexSolver.pc
+++ b/test/Solver/FastCexSolver.pc
@@ -1,4 +1,4 @@
-# RUN: %kleaver --use-fast-cex-solver --use-dummy-solver %s > %t
+# RUN: %kleaver --use-fast-cex-solver --solver-backend=dummy %s > %t
 # RUN: not grep FAIL %t
 
 array arr1[4] : w32 -> w8 = symbolic