Dear Armin Biere :
 
Thank you very much in confirming the result! It's really critical to output witnesses for sat instances, as you've mentioned.
 
Many thanks to your kindly reply and to run our checkers in a hurry.
 
 
BTW, I only received your message for describing some information about our checkers without the real template.
 
So I copy the one received by our multi-property checker "mpmc" as follows.
 
In case that there's anything we should also tell you or something we can help, please tell me then.
 
Thank you.
 
 
(A) name of the model checker (well I have this I think): v3 and v3i (two configurations)
(B) authors: Cheng-Yin Wu, Chi-An Wu, and Chung-Yang (Ric) Huang
(C) their affiliation: Cheng-Yin Wu and Chi-An Wu are PhD candidates from National Taiwan University, and Prof. Chung-Yang (Ric) Huang is our advisor.
(D) some bullets on the technology/algorithms, as well as to which extend the code is based on other tools:
       Solvers: BMC (with and without induction), PDR (2 versions, single and multiple solvers), and ITP (a new interpolation generation algorithm for SAT-based model checking, not published yet).
       We first simply (preprocess) the instance with ABC (linking ABC library to our framework) using SEC techniques in dprove  (reimplemented with different configurations / parameters from that in the standard command). Two solvers (one of them is BMC with induction) utilize 2 cores to solve the simplified instance. If each of them return SAT, back to solve the original instance using solvers (single solver PDR and BMC) which aimed at disproving the instance. The other two solvers (single solver PDR and BMC) occupy the remaining 2 cores to solve the original instance. Hence we can always output witnesses to the SAT instances.
      The difference between v3 and v3i is that v3 takes PDR (multiple solvers) as the other solver to solve the simplified instance while v3i adopts ITP (interpolation).
      We also share learned information (including inductive invariants, proved counterexample-free depth) among solvers.
 
(E) difference to previous versions if applicable: This is our first time to enter the competition.
 
 
Since we're unable to participate in FMCAD this year, it's a pity to have some discussion with you.
 
For the listed topics, we're interested in the first one: "word-level model checking".
 
Since the objective to develop v3 framework is to target on word-level (BV and RTL) model checking, we've implemented several existing algorithms for word-level model checking, including solvers above for this competition. Also, we've incorporated several SMT solvers, including Boolector. One of the problem we met is that we have too few word-level designs with challenging properties. (Compared to Boolean-level model checking, there are many hard instances from both academic and industry.) We are looking forward to a word-level model checking competition.
 
 
Thank you very much for holding HWMCC.
 
 
Best Regards,
Cheng-Yin