add release nodes and add the author reference in qfnra_tactic

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
Z3Prover · Aug 12, 2024 · bf34600 · bf34600
1 parent f2d35dd
commit bf34600
Show file tree

Hide file tree

Showing 2 changed files with 8 additions and 1 deletion.
diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
@@ -10,6 +10,13 @@ Version 4.next
     - native word level bit-vector solving.
   - introduction of simple induction lemmas to handle a limited repertoire of induction proofs.
 
+Version 4.13.1
+==============
+- single-sample cell projection in nlsat was designed by Haokun Li and Bican Xia. 
+- using simple-checker together with and variable ordering supported by qfnra_tactic was developed by Mengyu Zhao (Linxi) and Shaowei Cai.
+
+   The projection is described in paper by Haokun Li and Bican Xia,   [Solving Satisfiability of Polynomial Formulas By Sample - Cell Projection](https://arxiv.org/abs/2003.00409). The code ported from https://github.com/hybridSMT/hybridSMT.git 
+
 Version 4.13.0
 ==============
 - add ARM64 wheels for Python, thanks to Steven Moy, smoy

diff --git a/src/tactic/smtlogics/qfnra_tactic.h b/src/tactic/smtlogics/qfnra_tactic.h
@@ -12,7 +12,7 @@ Module Name:
 Author:
 
     Leonardo (leonardo) 2012-02-28
-
+    Mengyu Zhao (Linxi) and Shaowei Cai, ported from https://github.com/hybridSMT/hybridSMT.git
 Notes:
 
 --*/
-Original file line number
+Diff line change
@@ Expand Up / @@ -12,7 +12,7 @@ Module Name: @@
     Author:
         Leonardo (leonardo) 2012-02-28
+        Mengyu Zhao (Linxi) and Shaowei Cai, ported from https://github.com/hybridSMT/hybridSMT.git
     Notes:
     --*/
@@ Expand Down @@