diff --git a/Changelog.md b/Changelog.md
index 115f7a081..c25a3ef07 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -9,6 +9,7 @@ API changes:
 New features:
  - Implemented the interpolant production and incrementality for the Lookahead
  - Support for the combination of arrays and linear arithmetic (QF_ALIA, QF_AUFLIA)
+ - Implemented new solving heuristic - Picky CDCL, as an extension for the lookahead
 
 ### 2.4.3 (2022-11-21)
 
diff --git a/README.md b/README.md
index 21f96be15..fac00ca2d 100644
--- a/README.md
+++ b/README.md
@@ -88,6 +88,17 @@ $ opensmt test.smt2
 ```
 It is also possible to run OpenSMT without any arguments, in which case it reads the input from the standard input.
 
+### Other engines
+
+OpenSMT supports multiple SMT solving approaches. By the default it uses the approach described in the CoreSMTSolver. But it can also utilize 
+Lookahead or Picky CDCL. Those engines can be enabled by using following config:
+```
+(set-option :pure-lookahead true)
+```
+or
+```
+(set-option :picky true)
+```
 ### Interpolation
 OpenSMT supports a range of interpolation algorithms for propositional
 logic, linear real arithmetic, and uninterpreted functions with