summaryrefslogtreecommitdiff
path: root/src/main/driver_unified.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/main/driver_unified.cpp')
-rw-r--r--src/main/driver_unified.cpp5
1 files changed, 1 insertions, 4 deletions
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index ec3e10b5e..de7566b1f 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -143,7 +143,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
{
if( inputFromStdin ) {
// We can't do any fancy detection on stdin
- solver->setOption("input-language", "cvc");
+ solver->setOption("input-language", "smt2");
} else {
size_t len = filenameStr.size();
if(len >= 5 && !strcmp(".smt2", filename + len - 5)) {
@@ -151,9 +151,6 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
} else if((len >= 2 && !strcmp(".p", filename + len - 2))
|| (len >= 5 && !strcmp(".tptp", filename + len - 5))) {
solver->setOption("input-language", "tptp");
- } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) )
- || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) {
- solver->setOption("input-language", "cvc");
} else if((len >= 3 && !strcmp(".sy", filename + len - 3))
|| (len >= 3 && !strcmp(".sl", filename + len - 3))) {
// version 2 sygus is the default
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback