From: Junkie Dolphin (junkie.dolphin_at_libero.it)
Date: Tue Apr 19 2005 - 13:43:00 MDT
Hello everyone,
when bounded_model_check returns "formula undecided", but zchaff has died
trying to SAT-solving some CNF (for example, because it tried to malloc() too
much memory, and so on), the undecidability of the formula is simply due to the
abortion of zchaff, or one can say it is a "true" undecidability?
-- Ciao, Giovanni aka Junkie Dolphin Un augurio per le politiche 2006: Cantate ora, gente della torre di Anor, perché il regno di Sauron è finito per sempre, e la Torre Oscura è crollata. il "Canto dell'aquila", da "Il Signore degli anelli" *-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-* Fingerprint: 0380 DCDA F159 33B3 092D 0791 EB71 CD75 EF97 544D Get my public key with GnuPG: gpg --keyserver subkeys.pgp.net --recv-key 0xEF97544D *=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=*
This archive was generated by hypermail 2.1.7 : Mon Apr 18 2005 - 13:51:56 MDT