README changes

Author: Leo Alt

README.md

@@ -144,36 +144,54 @@ for (var contractName in output.contracts['test.sol']) {
 }
 ```
 
-The ``smtSolver`` callback function is used to solve SMT queries generated by
+Since version 0.5.1, the ``smtSolver`` callback function is used to solve SMT queries generated by
 Solidity's SMTChecker.  If you have an SMT solver installed locally, it can
 be used to solve the given queries, where the callback must synchronously
 return either an error or the result from the solver.  A default
-``smtSolver`` callback is distributed by ``solc-js``, which relies on either
-Z3 or CVC4 being installed locally.
+``smtSolver`` callback is included in this package via the module
+``smtchecker.js`` which exports the ``smtCallback`` function that takes 1) a
+function that takes queries and returns the solving result, and 2) a solver
+configuration object. The module ``smtsolver.js`` has a few pre defined solver
+configurations, and relies on Z3, Eldarica or CVC4 being installed locally.  It
+exports the list of locally found solvers and a function that invokes a given
+solver.
+
+The API of the SMT callback is **experimental** and can change at any time.
+The last change was in version 0.8.11.
 
 #### Example usage with smtSolver callback
 
 ```javascript
 var solc = require('solc');
-var smt = require('smtsolver');
+const smtchecker = require('solc/smtchecker');
+const smtsolver = require('solc/smtsolver');
 // Note that this example only works via node and not in the browser.
 
 var input = {
   language: 'Solidity',
   sources: {
     'test.sol': {
-      content: 'pragma experimental SMTChecker; contract C { function f(uint x) public { assert(x > 0); } }'
+      content: 'contract C { function f(uint x) public { assert(x > 0); } }'
+    }
+  },
+  settings: {
+    modelChecker: {
+      engine: "chc",
+      solvers: [ "smtlib2" ]
     }
   }
 };
 
 var output = JSON.parse(
-  solc.compile(JSON.stringify(input), { smtSolver: smt.smtSolver })
+  solc.compile(
+    JSON.stringify(input),
+    { smtSolver: smtchecker.smtCallback(smtsolver.smtSolver, smtsolver.availableSolvers[0]) }
+  )
 );
 
 ```
 The assertion is clearly false, and an ``assertion failure`` warning
-should be returned.
+should be returned, together with a counterexample.
 
 #### Low-level API