post-HWMCC13 changes to par.py

1 files changed, 100 insertions, 80 deletions

diff --git a/scripts/par.py b/scripts/par.py
index 110c5677..cbf4b12d 100644
--- a/scripts/par.py
+++ b/scripts/par.py
@@ -78,7 +78,7 @@ cex_list = []
 TERM = 'USL'
 last_gasp_time = 10000
 last_gasp_time = 500
-last_gasp_time = 900 #set to conform to hwmcc12
+last_gasp_time = 2001 #set to conform to hwmcc12
 use_pms = True
 
 #gabs = False #use the gate refinement method after vta
@@ -250,10 +250,10 @@ def initialize():
     cex_list = []
     n_pos_before = n_pos()
     n_pos_proved = 0
-    abs_time = 150
+    abs_time = 150 #timeout for abstraction
     abs_ref_time = 50 #number of sec. allowed for abstraction refinement.
-    total_spec_refine_time = 150
-    abs_ratio = .5
+    total_spec_refine_time = 150 # timeout for speculation refinement
+    abs_ratio = .5 
     hist = []
     skip_spec = False
     t_iter_start = 0
@@ -377,14 +377,16 @@ def set_engines(N=0):
     """
     global reachs,pdrs,sims,intrps,bmcs,n_proc,abs_ratio,ifbip,bmcs1, if_no_bip, allpdrs,allbmcs
     bmcs1 = [9] #BMC3
-    #for HWMCC we want to set N = 8
-    N = 8
+##    #for HWMCC we want to set N = 8
+##    N = 8
     if N == 0:
         N = n_proc = 1+os.sysconf(os.sysconf_names["SC_NPROCESSORS_ONLN"])
 ##        N = n_proc = 8 ### simulate 4 processors for HWMCC - turn this off a hwmcc.
     else:
         n_proc = N
 ##    print 'n_proc = %d'%n_proc
+    #strategy is to use 2x number of processors
+    N = n_proc = -1+2*N
     if N <= 1:
         reachs = [24]
         pdrs = [7]
@@ -733,6 +735,7 @@ def set_max_bmc(b):
         report_bmc_depth(max_bmc)
 
 def report_bmc_depth(m):
+    return #for non hwmcc applications
     print 'u%d'%m
 
 def print_circuit_stats():
@@ -941,7 +944,7 @@ def simplify(M=0,N=0):
                 print '\n'
     return get_status()
             
-def simulate2(t=900):
+def simulate2(t=2001):
     """Does rarity simulation. Simulation is restricted by the amount
     of memory it might use. At first wide but shallow simulation is done, followed by
     successively more narrow but deeper simulation. 
@@ -966,7 +969,7 @@ def simulate2(t=900):
             if ((time.clock()-btime) > t):
                 return 'UNDECIDED'
 
-def simulate(t=900):
+def simulate(t=2001):
     abc('&get')
     result = eq_simulate(t)
     return result
@@ -2094,7 +2097,7 @@ def speculate(t=0):
         write_file('spec')
         return Undecided_reduction
 
-def simple_sat(t=900):
+def simple_sat(t=2001):
     """
     aimed at trying harder to prove SAT
     """
@@ -2455,7 +2458,7 @@ def dsat_all(t=100,c=100000):
             break
     print 'Total time = %0.2f'%(time.time() - ttt)
             
-def check_sat(t=900):
+def check_sat(t=2001):
     """This is called if all the FF have disappeared, but there is still some logic left. In this case,
     the remaining logic may be UNSAT, which is usually the case, but this has to be proved. The ABC command 'dsat' is used fro combinational problems"""
     global smp_trace
@@ -3659,7 +3662,7 @@ def unmap_cex():
 ##    print 'cex matches original aig'
     
                                   
-def sp(n=0,t=900,check_trace=False):
+def sp(n=0,t=2001,check_trace=False):
     """Alias for super_prove, but also resolves cex to initial aig"""
     global initial_f_name
     print 'Executing super_prove'
@@ -3797,7 +3800,7 @@ def remove_v(ss,v):
             s = s + [ss[i]]
     return s
                  
-def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
+def multi_prove(op='simple',tt=2001,n_fast=0, final_map=[]):
     """two phase prove process for multiple output functions"""
     global max_bmc, init_initial_f_name, initial_f_name,win_list, last_verify_time
     global f_name_save,nam_save,_L_last,file_out
@@ -3809,7 +3812,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
     #handle single output case differently
     _L_last = [-1]*n_pos()
     if n_pos() == 1:
-        result = sp(2000)
+        result = sp(2001)
 ##        abc('w %s_unsolved.aig'%init_initial_f_name)
         rs=result[0]
         if rs == 'SAT':
@@ -3825,6 +3828,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
             L = [2]
         res = sumsize(L)
         rr = '\n@@@@ Time =  %d '%(time.time() - t_iter_start) + res
+        rr = '%s: '%init_initial_f_name + rr
         print rr
         file_out.write(rr+ '\n')
         file_out.flush()
@@ -3841,6 +3845,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
     rr = '\n@@@@ Time =  %.2f: '%(time.time() - t_iter_start)
     report_L(lst0,0) ##########
     rr = rr + res
+    rr = '%s: '%init_initial_f_name + rr
     print rr
     file_out.write(rr + '\n')
     file_out.flush()
@@ -3858,14 +3863,14 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
 ##    print S,lst1
     #put 0 values into lst0
     lst10 = indices(s,0) #new unsat POs in local indices (with lst0 removed)
-    if not lst10 == []:
-        print 'lst10 = %s'%str(lst10)
+##    if not lst10 == []:
+##        print 'lst10 = %s'%str(lst10)
     lst11 = indices(s,1) #local variables
     ss = expand(s,lst0,0) #ss will reflect original indices
     report_s(ss)
     lst0_old = lst0
     lst0 = indices(ss,0) #additional unsat POs added to initial lst0 (in original indices)
-    print 'lst0 = %s'%str(lst0)
+##    print 'lst0 = %s'%str(lst0)
     assert len(lst0) == len(lst0_old)+len(lst10), 'lst0 = %s, lst0_old = %s, lst10 = %s'%(str(lst0),str(lst0_old),str(lst10))
     sss = remove_v(ss,0) #remove the 0's from ss
     assert len(sss) == len(ss)-len(lst0), 'len(sss) = %d, len(ss) = %d, len(lst0) = %d'%(len(sss),len(ss),len(lst0))
@@ -3874,24 +3879,25 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
                 #done with new code
     assert len(lst1_1) == len(lst1), 'mismatch, lst1 = %d, lst1_1 = %d'%(len(lst1),len(lst1_1))
     lst1 = lst1_1 #lst1 should be in original minus lst0
-    print 'Found %d SAT POs'%len(lst1)
-    print 'Found %d UNSAT POs'%len(lst10)
+##    print 'Found %d SAT POs'%len(lst1)
+##    print 'Found %d UNSAT POs'%len(lst10)
     res = 'SAT = %d, UNSAT = %d, UNDECIDED = %d'%(len(lst1),len(lst0),NNN-(len(lst1)+len(lst0)))
     rr = '\n@@@@ Time =  %.2f: '%(time.time() - t_iter_start)
     rr = rr + res
+    rr = '%s: '%init_initial_f_name + rr
     print rr
     file_out.write(rr + '\n')
     file_out.flush()
     N = n_pos()
-    print len(lst10),n_pos()
+##    print len(lst10),n_pos()
     if not len(lst10) == n_pos() and len(lst10) > 0:
         remove(lst10,1) #remove 0 POs
         print 'Removed %d UNSAT POs'%len(lst10)
         N = n_pos()
     elif len(lst10) == n_pos():
         N = 0 #can't remove all POs. Must proceed as if there are no POs. But all POs are UNSAT.
-    print len(lst1),N,S #note: have not removed the lst1 POs.
-    if len(lst1) == N or S == 'UNSAT' or N == 0: #all POs are SAT
+##    print len(lst1),N,S #note: have not removed the lst1 POs.
+    if len(lst1) == N or S == 'UNSAT' or N == 0: #all POs are solved
         L = [0]*N #could just put L as all 1's. If N = 0, all POs are UNSAT and lst1 = []
         for i in range(len(lst1)): #put 1's in SAT POs
             L[lst1[i]]=1
@@ -3911,7 +3917,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
     else:
         N = 0
     if N == 1: #this was wrong. Need to report in original indices???
-        result = sp(2000)
+        result = sp(2001)
         rs=result[0]
         #need to find out original index of remaining PO
         if rs == 'SAT':
@@ -3928,6 +3934,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
         report_results(L)
         res = sumsize(L)
         rr = '\n@@@@ Time =  %d '%(time.time() - t_iter_start) + res
+        rr = '%s: '%init_initial_f_name + rr
         print rr
         file_out.write(rr+ '\n')
         file_out.flush()
@@ -3945,7 +3952,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
             map1 = create_map(leq,N) #creates map into original
 ##        print map1
             if not count_less(L,0) == N:
-                print L
+                print 'L = %s'%sumsize(L)
             L1 = [-1]*n_pos()
 ##        L1 = pass_down(L,list(L1),map1) # no need to pass down because L will have no values at this point.
         else:
@@ -3986,7 +3993,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
 ##        write_file('1')
 ##        L = output(list(L),list(L1),L2,map1,map2,lst0,lst1,NP)
         L = output2(list(L2),map1,map2,lst0,lst1,NP)
-        result = simple(2000,1)
+        result = simple(2001,1)
         Ss = rs = result[0]
         if rs == 'SAT':
             L2 = [1]
@@ -4030,7 +4037,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
             ttt = 20
         abc('w %s_before_mprove2.aig'%f_name)
         print '%s_before_mprove2.aig written'%f_name
-        print 'L2 = %s'%str(L2)
+##        print 'L2 = %s'%str(L2)
         print 'Entering first mprove2 for %d sec.'%ttt,
         Ss,L2 = mprove2(list(L2),op,ttt,1) #populates L2 with results
 ##        print Ss,L2
@@ -4104,7 +4111,7 @@ def multi_prove(op='simple',tt=900,n_fast=0, final_map=[]):
                     remove_proved_pos(L2)
                     simplify()
                     write_file('save')
-                    result = simple(2000,1)
+                    result = simple(2001,1)
                     if_found = False
                     if result[0] == 'UNSAT':
                         for i in range(N):
@@ -4147,6 +4154,7 @@ def multi_prove_iter():
     s = count_less(L,2) - (d+u)
     rr =  '\n@@@@@ %s: Final time =  %.2f '%(init_initial_f_name,(time.time() - t_iter_start))
     rr = rr + 'SAT = %d, UNSAT = %d, UNDECIDED = %d '%(s,u,d)
+    rr = '%s: '%init_initial_f_name + rr
     print rr
     file_out.write(rr)
     res = PO_results(L)
@@ -4534,6 +4542,7 @@ def report_results(L,final_map=[],if_final=False):
     print '\n'
 
 def report_result(POn, REn, final_map=[]):
+    return #for non hwmcc application
     if final_map == []:
         print 'PO = %d, Result = %d:  '%(POn, REn),
     else:
@@ -4608,7 +4617,7 @@ def scorr_T(t=10000):
     smp_trace = smp_trace + ['%s'%mtds[m_best]]
     abc('r %s_best_T.aig'%f_name)
 
-def pscorr(t=900):
+def pscorr(t=2001):
     result = par_scorr(t)
     if n_ands() == 0:
         return result
@@ -4738,9 +4747,9 @@ def mprove2(L=0,op='simple',t=100,nn=0):
         v = -1
         skip_spec_old = skip_spec
         skip_spec = True
-        result = simple(2000,1)
+        result = simple(2001,1)
         ff_name == f_name
-        result = sp(0,2000) #warning sp() can change f_name. 0 means simplify
+        result = sp(0,2001) #warning sp() can change f_name. 0 means simplify
         f_name = ff_name
         skip_spec = skip_spec_old
         res = result[0]
@@ -4784,7 +4793,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
         N = n_pos()
         tb = min(N,50)
 ##        print 'Trying par_multi_sat for %d sec.'%tb
-        S,lst1,s = par_multi_sat(tb,1,1,0) #this gives a list of SAT POs
+        S,lst1,s = par_multi_sat(tb,1,1,1) #this gives a list of SAT POs
         L2 = s10 = s
         n_solved = n_pos() - count_less(s10,0)
         if 1 in s10 or 0 in s10: #something solved 
@@ -4802,14 +4811,16 @@ def mprove2(L=0,op='simple',t=100,nn=0):
                     #iterate here as long as more than 1 PO is found SAT
                     n_solved = n_pos() - count_less(s210,0) 
                     while n_solved > 0:
+                        print 'n_solved = %d'%n_solved
                         gap = int(1+1.2*gap)
                         print 'gap = %.2f'%gap
                         pre_simp(1) #warning this may create const-0 pos
-                        S,lst2,s = par_multi_sat(tb,gap,1,0) #this can find UNSAT POs
+                        S,lst2,s = par_multi_sat(tb,gap,1,1) #this can find UNSAT POs
                         s210 = s
                         n_solved = n_pos() - count_less(s210,0)
                         s10 = put(s210,list(s10)) #put the new values found into s10
                         if count_less(s10,0) == 0 or n_solved == 0: #all solved or nothing solved
+                            print 's210 = %s'%sumsize(s210)
                             break #s10 has the results
                         else:
                             out = '\n@@@@ Time = %.2f: additional POs found SAT = %d'%((time.time()- t_iter_start),len(lst2))
@@ -4821,7 +4832,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
                             remove(rem,1) #this zeros the l210 and then removes ALL const-1 POs.
                                             #If there are more than lst2 removed, it fires an assertion.
                             continue
-                    L2 = s10 #put results in s10
+                    L2 = s10 #put results of s10 into L2
                 else: #lst1 is empty or S == SAT'
                     print 'no cex found or S = UNSAT'
             else: #all solved
@@ -4833,7 +4844,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
         if -1 in s10:
             print 'Entering solve_all ',
             ps()
-            S,s210 = solve_all([-1]*n_pos(),900) #solve_all calls sp() or simple but preserves the aig and f_name
+            S,s210 = solve_all([-1]*n_pos(),2001) #solve_all calls sp() or simple but preserves the aig and f_name
 ##            else: zzz
             if -1 in s210: #then no POs were solved by solve_all
 ##                abc('r %s_smp2_2.aig'%f_name)
@@ -4846,7 +4857,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
                     s210 = [-1]*n_pos()
             print 's210 after mprove and before inject 1 %s:'%sumsize(s210)
             L2 = put(s210,s10) 
-            print 'L2 after inject 1 %s:'%sumsize(L2)
+##            print 'L2 after inject 1 %s:'%sumsize(L2)
         else: #all POs solved
             L2 = s10
         assert NP == 1, 'NP > 1: ERROR'
@@ -4857,7 +4868,7 @@ def mprove2(L=0,op='simple',t=100,nn=0):
             print 'L1 after unmap of map3: ',
             print sumsize(L1)
         else:
-            print 'L2 = %s'%str(L2)
+##            print 'L2 = %s'%str(L2)
             L1 = L2
         L1 = inject(list(L1),Llst0,0)
         print 'L1 after inject of Llst0 0s: %s:'%sumsize(L1)
@@ -4969,10 +4980,10 @@ def solve_all(L2,t):
 ##    ps()
     skip_spec_old = skip_spec
     skip_spec = True
-    tt = max(t,900)
+    tt = max(t,2001)
     print 'Entering simple for %d sec.'%tt
-    result = simple(tt,1) #### temporary 1 means do not simplify
-##    result = sp(0,t) #warning sp() may change f_name
+##    result = simple(tt,1) #### temporary 1 means do not simplify
+    result = sp(0,t) #warning sp() may change f_name. Changed from HWMCC13 submission
     skip_spec = skip_spec_old
 ##    print 'solve_all: result = %s'%result
     if result[0] == 'UNSAT':
@@ -5147,7 +5158,7 @@ def mprove(L,op='simple',tt=1000):
 ##    sec_options = options
 ##    return super_prove(1)
 
-def super_prove(n=0,t=900):
+def super_prove(n=0,t=2001):
     """Main proof technique now. Does original prove and if after speculation there are multiple output left
     if will try to prove each output separately, in reverse order. It will quit at the first output that fails
     to be proved, or any output that is proved SAT
@@ -5358,13 +5369,13 @@ def reachn(t):
     print 'reachm3 done in time = %f'%(time.clock() - x)
     return get_status()
     
-def reachx(t=900):
+def reachx(t=2001):
     x = time.time()
     abc('reachx -t %d'%t)
     print 'reachx  done in time = %f'%(time.time() - x)
     return get_status()
 
-def reachy(t=900):
+def reachy(t=2001):
     x = time.clock()
     abc('&get;&reachy -v -T %d'%t)
 ##    print 'reachy done in time = %f'%(time.clock() - x)
@@ -6033,18 +6044,18 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
         t = gt
     last_gap = gt
 ##    H = max(100, t/n_pos()+1)
-    if not H == 0:
+    if not H == 0: #se timeout peer output
         H = (gt*1000)/n_pos()
         H = max(min(H,1000*gt),100)
     tme = time.time()
     list0 = listr_0_pos() #reduces POs
     list0.sort()
 ##    print 'list0 = %s'%str(list0)
-    if len(list0)>0:
-        print 'temporarily removed %d cost-0 POs'%len(list0)
-    ps()
+##    if len(list0)>0:
+##        print 'removed %d cost-0 POs'%len(list0)
+##    ps()
     if len(list0)> 0:
-        print 'Found %d const-0 POs, but not removed'%len(list0)
+        print 'Found initial %d const-0 POs'%len(list0)
 ##        print ll
     print 'par_multi_sat entered for %.2f sec. and gap = %.2f  sec., H = %.2f'%(t,gt,H)
     base = m*1000
@@ -6054,10 +6065,10 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
     mx = 1000000000/max(1,n_latches())
     N = n_pos()
     na = n_ands()
-    F = [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,H))'%(0*base))]
+    F = [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,H))'%(0))]
 ##    if na < 50000:
     F = F + [eval('(pyabc_split.defer(pdraz)(t,gt,H))')] #need pdr in??
-    F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(0*base))]
+    F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(0))]
     F = F + [eval('(pyabc_split.defer(sleep)(t))')]
     F = F + [eval('(pyabc_split.defer(sim3az)(t,gt,%d,4,0))'%(100))]
     F = F + [eval('(pyabc_split.defer(bmc3az)(t,gt,%d,0))'%(100))]
@@ -6087,8 +6098,8 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
     nn = len(F)
     for i,res in pyabc_split.abc_split_all(F):
         ii = ii + [i]
-        if len(ii) == len(F)-1: #all done but sleep
-            break
+##        if len(ii) == len(F)-1: #all done but sleep
+##            break
         if i == 3: #sleep timeout
             print 'sleep timeout'
             break
@@ -6097,15 +6108,15 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
 ####        print i
         if i == 0:
             zero_done = True # bmc with start at 0 is done
-        if i == 2:
+        if i == 2: #sim3 with start 0 is done
             two_done = True
         if res == None: #this can happen if one of the methods bombs out
             print 'Method %d returned None'%i
             continue
 ##        print res
-        s1 = switch(res[1]) #res[1]= s
-        s = merge_s(list(s),s1)
-        print sumsize(s)
+        s1 = switch(list(res[1])) #res[1]= s
+        s = merge_s(list(s),s1) 
+##        print sumsize(s)
         ss = ss + [s1]
 ##        LL = LL + [res[0]]
 ##        L = L + res[0]
@@ -6127,25 +6138,27 @@ def par_multi_sat(t=10,gap=0,m=1,H=0):
             r = ss2[0]
             if r == ss2[1] and count_less(r,1) < len(r): #at least 1 SAT PO found
                 break
+        if len(ii) == len(F)-1: #all done but sleep
+            break
 ##        if len(LL) > 1 and zero_done and two_done:
 ##            ll2 = LL[-2:] #checking if last 2 results agree
 ##            if ll2[0] == ll2[1] and ll2[0] > 0:
 ##                break
-    print 'Found %d SAT POs in '%(len(L)),
+##    print 'Found %d SAT POs in '%(len(L)),
     print 'time = %.2f'%(time.time()-tme)
-    print sumsize(s)
+##    print sumsize(s)
 ##    L.sort()
 ##    print 'L_before = %s'%(str(L))
 ####    check_None_status(L,s,1) #now 1 in s means sat. s can have 0 in it, meaning it found some POs unsat.
 ##    L = merge(list(list0),list(L),1) #shift L according to list0 but do not include list0.
 ##    print 'L_shifted = %s'%(str(L))
 ##    # Need to return only SAT POs have to do the same for s
-    print 'len(s) = %d, len(list0) = %d'%(len(s),len(list0))
+##    print 'len(s) = %d, len(list0) = %d'%(len(s),len(list0))
     ss = expand(s,list0,0)
 ##    assert list0 == indices(ss,0)
-    print sumsize(ss)
+    print '\n Par_multi_sat result = %s'%sumsize(ss)
 ##    assert check_consistancy(L,ss), 'inconsistant'
-    abc('r %s_save.aig'%f_name)
+    abc('r %s_save.aig'%f_name) #restore initial aig
     return S,[],ss
 
 
@@ -6334,7 +6347,7 @@ def remove_proved_pos(lst):
 
 
         
-def bmc_j(t=900):
+def bmc_j(t=2001):
     """ finds a cex in t seconds starting at 2*N where N is depth of bmc -T 1"""
     x = time.time()
     tt = min(5,max(1,.05*t))
@@ -6354,7 +6367,7 @@ def bmc_j(t=900):
 ##        print 'cex found in %0.2f sec at frame %d'%((time.time()-x),cex_frame())
     return RESULT[get_status()]
 
-def pdrseed(t=900):
+def pdrseed(t=2001):
     """uses the abstracted version now"""
 ##    abc('&get;,treb -rlim=60 -coi=3 -te=1 -vt=%f -seed=521'%t)
     abc('&get;,treb -rlim=100 -vt=%f -seed=521'%t)
@@ -6364,20 +6377,20 @@ def pdrold(t):
     abc('&get; ,pdr -vt=%f'%t)
     return RESULT[get_status()]
 
-def pdr(t=900):
+def pdr(t=2001):
     abc('&get; ,treb -vt=%f'%t)
     return RESULT[get_status()]
 
-def pdr0(t=900):
+def pdr0(t=2001):
     abc('&get; ,pdr -rlim=100 -vt=%f'%t)
     return RESULT[get_status()]
 
-def pdra(t=900):
+def pdra(t=2001):
 ##    abc('&get; ,treb -rlim=100 -ssize -pre-cubes=3 -vt=%f'%t)
     abc('&get; ,treb -abs -rlim=100 -sat=abc -vt=%f'%t)
     return RESULT[get_status()]
 
-def pdrm(t=900):
+def pdrm(t=2001):
     abc('pdr -C 0 -T %f'%t)
     return RESULT[get_status()]
 
@@ -6389,30 +6402,37 @@ def bmc2(t):
    abc('bmc2 -C 1000000 -T %f'%t)
    return RESULT[get_status()]
 
-def bmc(t=900):
+def bmc(t=2001):
     abc('&get; ,bmc -vt=%d'%t)
     return RESULT[get_status()]
 
-def intrp(t=900):
+def intrp(t=2001):
     abc('&get; ,imc -vt=%d'%t)
     return RESULT[get_status()]
 
-def bmc3az(t=900,gt=10,C=999,H=0):
+def bmc3az(t=2001,gt=10,C=999,H=0):
     t_init = time.time()
-    if  C > 999:
+    if  not C == 0:
         abc('&get; &cycle -F %d; &put'%C) 
-    abc('bmc3 -az -C 1000000 -T %d -G %d -H %.2f'%(t,gt,H))
+    abc('bmc3 -az -C 1000000 -T %.2f -G %.2f -H %.2f'%(t,gt,H))
     cex_list = cex_get_vector()
     L = list_non_None(cex_list)
 ##    check_None_status(L)
-    print 'bmc3az(%.2f,%.2f,%d,%d): CEXs = %d, time = %.2f'%(t,gt,C,H,len(L),(time.time()-t_init))
-##    s = status_get_vector()
-    s = [-1]*n_pos()
-    for j in L:
-        s[j]=0 #0 here means SAT. It will be switched in par_multi_sat
+    print '\nbmc3az(%.2f,%.2f,%d,%d): CEXs = %d, time = %.2f'%(t,gt,C,H,len(L),(time.time()-t_init))
+    print 'Length CEXs = %d'%(len(L))
+    s = status_get_vector()
+    if len(s) == 0: #error if this happens check with Alan
+        s = [-1]*n_pos()
+    sss = switch(list(s))
+    print 's_status = %s'%sumsize(sss)
+##    s = [-1]*n_pos()
+##    for j in L:
+##        s[j]=0 #0 here means SAT. It will be switched in par_multi_sat
+##    sss = switch(list(s))
+##    print 's = %s'%sumsize(sss)
     return L,s
 
-def pdraz(t=900,gt=10,H=0):
+def pdraz(t=2001,gt=10,H=0):
     print 'pdraz entered with t = %.2f, gt = %.2f, H = %.2f'%(t,gt,H)
     t_init = time.time()
     run_command('pdr -az -T %d -G %d -H %.2f'%(t,gt,H))
@@ -6427,10 +6447,10 @@ def pdraz(t=900,gt=10,H=0):
     print 'pdraz(%.2f,%.2f,%d): CEXs = %d, time = %.2f'%(t,gt,H,len(L),(time.time()-t_init))
     return L,s
 
-def sim3az(t=900,gt=10,C=1000,W=5,N=0):
+def sim3az(t=2001,gt=10,C=1000,W=5,N=0):
     """ N = random seed, gt is gap time, W = # words, F = #frames"""
     t_init = time.time()
-    if  C > 1000:
+    if  not C == 0:
         abc('&get; &cycle -F %d; &put'%C) 
     abc('sim3 -az -T %.2f -G %.2f -F 40 -W %d -N %d'%(t,gt,W,N))
     cex_list = cex_get_vector()
@@ -6442,11 +6462,11 @@ def sim3az(t=900,gt=10,C=1000,W=5,N=0):
     print 'sim3az(%.2f,%.2f,%d,%d,%d): CEXs=%d, time = %.2f'%(t,gt,C,W,N,len(L),(time.time()-t_init))
     return L,s
     
-def bmc3(t=900):
+def bmc3(t=2001):
     abc('bmc3 -C 1000000 -T %d'%t)
     return RESULT[get_status()]
 
-def intrpm(t=900):
+def intrpm(t=2001):
     abc('int -C 1000000 -F 10000 -K 1 -T %d'%t)
     print 'intrpm: status = %d'%get_status() 
     return RESULT[get_status()]