diff --git a/NEWS.md b/NEWS.md index 8c7997a..75a3ebc 100644 --- a/NEWS.md +++ b/NEWS.md @@ -1,7 +1,9 @@ This file contains a summary of important user-visible changes. -ethos 0.1.1 prerelease -====================== +ethos 0.1.1 +=========== + +This release of Ethos is associated with the 1.2.1 release of the SMT solver cvc5. - When parsing Eunoia signatures, decimals and hexidecimals are never normalized, variables in binders are always unique for their name and type, and let is never treated as a builtin way of specifying macros. The options `--no-normalize-dec`, `--no-normalize-hex`, `--binder-fresh`, and `--no-parse-let` now only apply when parsing proofs and reference files. - Adds a new option `--normalize-num`, which also only applies when reference parsing. This option treats numerals as rationals, which can be used when parsing SMT-LIB inputs in logics where numerals are shorthand for rationals. diff --git a/src/main.cpp b/src/main.cpp index 3134a45..43f3bdf 100644 --- a/src/main.cpp +++ b/src/main.cpp @@ -79,12 +79,14 @@ int main( int argc, char* argv[] ) out << " -t : enables the given trace tag (requires debug build)." << std::endl; out << " -v: verbose mode, enable all standard trace messages (requires debug build)." << std::endl; std::cout << out.str(); + // exit immediately + exit(0); return 0; } else if (arg=="--show-config") { std::stringstream out; - out << "This is ethos version 0.1.0." << std::endl; + out << "This is ethos version 0.1.1." << std::endl; out << std::endl; size_t w = 15; out << std::setw(w) << "tracing : "; @@ -95,6 +97,8 @@ int main( int argc, char* argv[] ) #endif out << std::endl; std::cout << out.str(); + // exit immediately + exit(0); return 0; } else if (arg=="-t")