note that pysmt also supports portfolio + incrementalHEADmaster

1 files changed, 4 insertions, 3 deletions

diff --git a/README b/README
index 3463ad6..705abed 100644
--- a/README
+++ b/README
@@ -32,16 +32,17 @@ More details on persistent caching:
     satispipy will return immediately for the third call
     if you run the program again, it will also return immediately for all calls
 
-More details on portfolio solving:
+portfolio + incremental:
     portfolio is hard to make work with incremental solving.
     suppose you're portfolio solving with solvers SMTA and SMTB,
     and make incremental queries X, Y, Z
     what if SMTA is fast for X and Y, but slow for Z? and SMTB is the opposite
     we might have to wait for SMTA to solve X and Y before it gets to Z
 
-    instead, after each solve, we kill all but the single solver that solved it
+    like pysmt
+    (https://github.com/pysmt/pysmt/blob/8c79de2635936f980595f4a43ee20a7da7554844/pysmt/solvers/portfolio.py#L87),
+    after each solve we kill all but the single solver that solved it
     so SMTB starts fresh on the calls for Y and Z
-    no need to wait
 
 Quantifier instantiation:
     top-level assertions can be universally quantified