--- /dev/null
+Buildfile: /scratch/satcheck/satproject/constraint_compiler/src/Benchmarks/sypet/build.xml
+
+sypet:
+ [java] ----------Options
+ [java] Verbose: false
+ [java] Timeout: 600000
+ [java] Round Robin: true
+ [java] Round Robin Iterations: 100
+ [java] Round Robin Range: 2
+ [java] Solver limit: 5
+ [java] ----------benchmarks/xml/24/benchmark24.json
+ [java] Benchmark Id: 24
+ [java] Method name: getParagraphElement
+ [java] Packages: [javax.swing.text]
+ [java] Libraries: [./lib/rt7.jar]
+ [java] Source type(s): [javax.swing.text.Document, int]
+ [java] Target type: javax.swing.text.Element
+ [java] --------------------------------------------------------
+ [java] Warning: javax.crypto.spec.DESKeySpec is a phantom class!
+ [java] Warning: javax.crypto.spec.DESedeKeySpec is a phantom class!
+ [java] Warning: javax.crypto.Cipher is a phantom class!
+ [java] Warning: javax.crypto.spec.SecretKeySpec is a phantom class!
+ [java] Warning: javax.crypto.SecretKeyFactory is a phantom class!
+ [java] Warning: javax.crypto.spec.IvParameterSpec is a phantom class!
+ [java] Warning: javax.crypto.SecretKey is a phantom class!
+ [java] Warning: javax.crypto.spec.PBEKeySpec is a phantom class!
+ [java] Warning: javax.crypto.Mac is a phantom class!
+ [java] Warning: javax.crypto.IllegalBlockSizeException is a phantom class!
+ [java] Warning: javax.crypto.BadPaddingException is a phantom class!
+ [java] Warning: javax.crypto.NoSuchPaddingException is a phantom class!
+ [java] Warning: sun.security.ssl.Krb5Helper is a phantom class!
+ [java] Warning: com.oracle.jrockit.jfr.FlightRecorder is a phantom class!
+ [java] Warning: sun.security.ssl.SSLSocketImpl is a phantom class!
+ [java] Warning: javax.crypto.CipherInputStream is a phantom class!
+ [java] Warning: javax.crypto.CipherOutputStream is a phantom class!
+ [java] Warning: sun.nio.cs.ext.EUC_TW$Decoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.EUC_TW$Encoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.DoubleByteEncoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.JIS_X_0201$Encoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.JIS_X_0201$Decoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.JIS_X_0208_Encoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.JIS_X_0208_Decoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.JIS_X_0212_Encoder is a phantom class!
+ [java] Warning: sun.nio.cs.ext.JIS_X_0212_Decoder is a phantom class!
+ [java] Warning: javax.crypto.spec.PBEParameterSpec is a phantom class!
+ [java] Warning: javax.crypto.spec.DHParameterSpec is a phantom class!
+ [java] Warning: javax.crypto.spec.DHPublicKeySpec is a phantom class!
+ [java] Warning: javax.crypto.interfaces.DHKey is a phantom class!
+ [java] Warning: javax.crypto.interfaces.DHPublicKey is a phantom class!
+ [java] Warning: javax.crypto.spec.OAEPParameterSpec is a phantom class!
+ [java] Warning: javax.crypto.spec.PSource is a phantom class!
+ [java] Warning: javax.crypto.spec.PSource$PSpecified is a phantom class!
+ [java] Warning: javax.crypto.KeyGenerator is a phantom class!
+ [java] #Classes: 441
+ [java] #Methods: 4076
+ [java] Soot Time: 3542.019569
+ [java] PetriNet for path length: 1 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] PetriNet for path length: 2 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] PetriNet for path length: 3 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] PetriNet for path length: 4 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] PetriNet for path length: 5 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] Path Solving Time: 41.694771
+ [java] Path Solving Time: 9.796036
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756712337 Original Encoding Solving Time: 0.498818
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756712337Satune Solving Time: 31.387467
+ [java] Done with finding holes : Flag = false
+ [java] 1594756715226 Original Encoding Solving Time: 0.05699
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756715226Satune Solving Time: 0.077839
+ [java] Path Solving Time: 26.469597
+ [java] Path Solving Time: 12.911085
+ [java] Path Solving Time: 29.683449
+ [java] PetriNet for path length: 6 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] Renaming procedure ...
+ [java] Path Solving Time: 20.021253
+ [java] Path Solving Time: 4.025236
+ [java] 1594756717381 Original Encoding Solving Time: 3.218729
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756717381Satune Solving Time: 44.816314
+ [java] 1594756717457 Original Encoding Solving Time: 0.058897
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756717457Satune Solving Time: 0.085318
+ [java] Path Solving Time: 28.849032
+ [java] Path Solving Time: 4.209647
+ [java] Path Solving Time: 17.364188
+ [java] Path Solving Time: 47.181145
+ [java] Path Solving Time: 83.448103
+ [java] 1594756717679 Original Encoding Solving Time: 1.014008
+ [java] Polarity time: 0.000033
+ [java] Preprocess time: 0.000024
+ [java] Decompose Order: 0.000017
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4f85b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4f87f0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4f86d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4f8960....
+ [java] Encoding Graph Time: 0.000153
+ [java] Elapse Encode time: 0.000285
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 9 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000001
+ [java] SAT Solving time: 0.031047
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.031346
+ [java] Elapse Encode time: 0.000041
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000049
+ [java] serializing ...
+ [java] {BooleanPredicate<0x7fec5c503a90>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c4f85b0>:{Set(1)<0x7fec5c7cf0c0>:Members: 5, } 0x7fec5c4f85b0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c7eaaa0>: 5}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7fec5c503b00>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c7ca800>:{Set(1)<0x7fec5c7ea850>:Members: 6, } 0x7fec5c7ca800 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c7ea8b0>: 6}
+ [java] }
+ [java]
+ [java] !{BooleanLogic<0x7fec5c4fe0a0>: AND
+ [java] !{BooleanPredicate<0x7fec5c7e8be0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c7eb650>:{Set(1)<0x7fec5c7eb7d0>:Members: 7, } 0x7fec5c7eb650 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c7ea750>: 7}
+ [java] }
+ [java] !{BooleanPredicate<0x7fec5c503a20>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c9888f0>:{Set(1)<0x7fec5c280170>:Members: 7, 8, } 0x7fec5c9888f0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c7ea750>: 7}
+ [java] }
+ [java] !{BooleanPredicate<0x7fec5c238ab0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c4feb90>:{Set(1)<0x7fec5c7e6340>:Members: 7, 8, 9, } 0x7fec5c4feb90 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c7ea750>: 7}
+ [java] }
+ [java] }
+ [java]
+ [java] !{BooleanLogic<0x7fec5c4fcda0>: AND
+ [java] !{BooleanPredicate<0x7fec5c4b8130>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c9888f0>:{Set(1)<0x7fec5c280170>:Members: 7, 8, } 0x7fec5c9888f0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c4761f0>: 8}
+ [java] }
+ [java] !{BooleanPredicate<0x7fec5c4b80c0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c4feb90>:{Set(1)<0x7fec5c7e6340>:Members: 7, 8, 9, } 0x7fec5c4feb90 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c4761f0>: 8}
+ [java] }
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7fec5c4fcf70>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5c4feb90>:{Set(1)<0x7fec5c7e6340>:Members: 7, 8, 9, } 0x7fec5c4feb90 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5c243b70>: 9}
+ [java] }
+ [java]
+ [java] Polarity time: 0.000009
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4f85b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c7ca800....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c7eb650....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9888f0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4feb90....
+ [java] Encoding Graph Time: 0.000119
+ [java] Elapse Encode time: 0.000156
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044642
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044805
+ [java] Elapse Encode time: 0.000026
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000046
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c7eb650....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4b73b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4b7330....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c4f85b0....
+ [java] Encoding Graph Time: 0.0isSat= true ,SatuneSat= true
+ [java] 1594756717679Satune Solving Time: 35.997073
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: RTFParser is not public in javax.swing.text.rtf; cannot be accessed from outside package
+ [java] javax.swing.text.Element sypet_var12 = sypet_arg0.getDefaultRootElement();javax.swing.text.rtf.RTFParser sypet_var13 = new javax.swing.text.rtf.RTFParser();sypet_var13.writeSpecial(sypet_arg1);return sypet_var12;}
+ [java] ^
+ [java] /Source.java:3: error: RTFParser is not public in javax.swing.text.rtf; cannot be accessed from outside package
+ [java] javax.swing.text.Element sypet_var12 = sypet_arg0.getDefaultRootElement();javax.swing.text.rtf.RTFParser sypet_var13 = new javax.swing.text.rtf.RTFParser();sypet_var13.writeSpecial(sypet_arg1);return sypet_var12;}
+ [java] ^
+ [java] 2 errors
+ [java] Path Solving Time: 9.997381
+ [java] Path Solving Time: 11.450115
+ [java] Path Solving Time: 30.654587
+ [java] 1594756718001 Original Encoding Solving Time: 0.5018
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756718001Satune Solving Time: 53.288832
+ [java] Path Solving Time: 9.400433
+ [java] Path Solving Time: 47.349647
+ [java] Path Solving Time: 9.599939
+ [java] 1594756718195 Original Encoding Solving Time: 0.4491
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756718195Satune Solving Time: 55.73952
+ [java] Path Solving Time: 8.987005
+ [java] Path Solving Time: 12.209779
+ [java] Path Solving Time: 7.398769
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: JTextComponent is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var27 = sypet_arg0.getDefaultRootElement();javax.swing.text.JTextComponent sypet_var28 = new javax.swing.text.JTextComponent();sypet_var28.setSelectionStart(sypet_arg1);return sypet_var27;}
+ [java] ^
+ [java] 1 error
+ [java] 1594756718342 Original Encoding Solving Time: 0.650323
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756718342Satune Solving Time: 44.583495
+ [java] Path Solving Time: 9.188267
+ [java] Path Solving Time: 37.093286
+ [java] Path Solving Time: 5.306434
+ [java] 1594756718500 Original Encoding Solving Time: 0.27269
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756718500Satune Solving Time: 42.691844
+ [java] Path Solving Time: 8.495446
+ [java] Path Solving Time: 11.636438
+ [java] Path Solving Time: 5.053668
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: JTextComponent is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var37 = sypet_arg0.getDefaultRootElement();javax.swing.text.JTextComponent sypet_var38 = new javax.swing.text.JTextComponent();sypet_var38.setSelectionEnd(sypet_arg1);return sypet_var37;}
+ [java] ^
+ [java] 1 error
+ [java] 1594756718640 Original Encoding Solving Time: 0.266374
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756718640Satune Solving Time: 42.897441
+ [java] Path Solving Time: 12.217027
+ [java] Path Solving Time: 10.542962
+ [java] Path Solving Time: 7.292831
+ [java] 1594756718774 Original Encoding Solving Time: 0.384909
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 00070
+ [java] Elapse Encode time: 0.000096
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.035886
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.035989
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000018
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca5ad90....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca5b070....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca5b1e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca5af00....
+ [java] Encoding Graph Time: 0.000155
+ [java] Elapse Encode time: 0.000202
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.053068
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.053279
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000011
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca29330....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca30150....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca294a0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca302c0....
+ [java] Encoding Graph Time: 0.000118
+ [java] Elapse Encode time: 0.000155
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.055571
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.055733
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9cca60....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9cc960....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9cc5e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9cc9e0....
+ [java] Encoding Graph Time: 0.000120
+ [java] Elapse Encode time: 0.000152
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.044416
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.044575
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9e5e10....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9e5d10....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9e5d90....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9e5c90....
+ [java] Encoding Graph Time: 0.000109
+ [java] Elapse Encode time: 0.000139
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.042537
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.042684
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9f91d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9f9430....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9f95a0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c9f92e0....
+ [java] Encoding Graph Time: 0.000070
+ [java] Elapse Encode time: 0.000092
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.042792
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.042889
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca84b30....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca84a30....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca849b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca84ab0....
+ [java] Encoding Graph Time: 0.000104
+ [java] Elapse Encode time: 0.000130
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.0588isSat= true ,SatuneSat= true
+ [java] 1594756718774Satune Solving Time: 59.032731
+ [java] Path Solving Time: 7.527936
+ [java] Path Solving Time: 5.494461
+ [java] Path Solving Time: 4.769413
+ [java] 1594756718914 Original Encoding Solving Time: 3.391028
+ [java] Renaming procedure ...
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756718914Satune Solving Time: 41.399766
+ [java] Path Solving Time: 8.43785
+ [java] Path Solving Time: 7.543986
+ [java] Path Solving Time: 5.498842
+ [java] 1594756719036 Original Encoding Solving Time: 0.344198
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: JTextComponent is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var52 = sypet_arg0.getDefaultRootElement();javax.swing.text.JTextComponent sypet_var53 = new javax.swing.text.JTextComponent();sypet_var53.moveCaretPosition(sypet_arg1);return sypet_var52;}
+ [java] ^
+ [java] 1 error
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756719036Satune Solving Time: 41.479885
+ [java] Path Solving Time: 8.454799
+ [java] Path Solving Time: 6.432311
+ [java] Path Solving Time: 5.29107
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756719171 Original Encoding Solving Time: 0.356707
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756719171Satune Solving Time: 41.308261
+ [java] Path Solving Time: 8.458273
+ [java] Path Solving Time: 7.402937
+ [java] Path Solving Time: 5.292236
+ [java] 1594756719288 Original Encoding Solving Time: 0.290991
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756719288Satune Solving Time: 42.708888
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: JTextComponent is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var62 = sypet_arg0.getDefaultRootElement();javax.swing.text.JTextComponent sypet_var63 = new javax.swing.text.JTextComponent();sypet_var63.setCaretPosition(sypet_arg1);return sypet_var62;}
+ [java] ^
+ [java] 1 error
+ [java] Path Solving Time: 7.747169
+ [java] Path Solving Time: 61.721392
+ [java] Path Solving Time: 5.219111
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: AbstractFilter is not public in javax.swing.text.rtf; cannot be accessed from outside package
+ [java] javax.swing.text.rtf.AbstractFilter sypet_var67 = new javax.swing.text.rtf.AbstractFilter();sypet_var67.write(sypet_arg1);javax.swing.text.Element sypet_var69 = sypet_arg0.getDefaultRootElement();return sypet_var69;}
+ [java] ^
+ [java] /Source.java:3: error: AbstractFilter is not public in javax.swing.text.rtf; cannot be accessed from outside package
+ [java] javax.swing.text.rtf.AbstractFilter sypet_var67 = new javax.swing.text.rtf.AbstractFilter();sypet_var67.write(sypet_arg1);javax.swing.text.Element sypet_var69 = sypet_arg0.getDefaultRootElement();return sypet_var69;}
+ [java] ^
+ [java] 1594756719460 Original Encoding Solving Time: 0.512313
+ [java] 85
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.059025
+ [java] Setting UNSAT %%%
+ [java] serializing ...
+ [java] {BooleanPredicate<0x7fec5ca9c0a0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5ca9c190>:{Set(1)<0x7fec5ca9cce0>:Members: 45, } 0x7fec5ca9c190 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5ca78360>: 45}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7fec5ca78690>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5ca9c490>:{Set(1)<0x7fec5ca780a0>:Members: 46, } 0x7fec5ca9c490 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5ca78590>: 46}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7fec5ca78930>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5ca78210>:{Set(1)<0x7fec5ca78190>:Members: 47, } 0x7fec5ca78210 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5ca78830>: 47}
+ [java] }
+ [java]
+ [java] {BooleanPredicate<0x7fec5ca78bd0>:
+ [java] PredicateOperator: ==
+ [java] elements:
+ [java] {ElementSet<0x7fec5ca848b0>:{Set(1)<0x7fec5ca77fb0>:Members: 48, } 0x7fec5ca848b0 UNASSIGNED numVars= 0 encArraySize= 0}{ElementConst<0x7fec5ca78ad0>: 48}
+ [java] }
+ [java]
+ [java] Polarity time: 0.000003
+ [java] Preprocess time: 0.000005
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca9c190....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca9c490....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca78210....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca848b0....
+ [java] Encoding Graph Time: 0.000070
+ [java] Elapse Encode time: 0.000087
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.041299
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.041392
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cab4ce0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cab4810....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cab48e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cab4c60....
+ [java] Encoding Graph Time: 0.000087
+ [java] Elapse Encode time: 0.000113
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.041355
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.041473
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cace260....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cace160....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cace0e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cace1e0....
+ [java] Encoding Graph Time: 0.000065
+ [java] Elapse Encode time: 0.000089
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.041208
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.041301
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cae6c00....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cae67b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cace060....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cae6b80....
+ [java] Encoding Graph Time: 0.000061
+ [java] Elapse Encode time: 0.000084
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.042612
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.042701
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5caffd70....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5caffdf0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5caffe70....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5caffcf0....
+ [java] Encoding Graph Time: 0.000086
+ [java] Elapse Encode time: 0.000135
+ [java] Is problem UNSAT after encoding: 0
+ [java] #isSat= true ,SatuneSat= true
+ [java] 1594756719460Satune Solving Time: 41.835133
+ [java] Path Solving Time: 8.871495
+ [java] 2 errors
+ [java] Path Solving Time: 85.829089
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] Done with finding holes : Flag = false
+ [java] 1594756719647 Original Encoding Solving Time: 0.33959
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756719647Satune Solving Time: 41.413592
+ [java] 1594756719705 Original Encoding Solving Time: 0.039869
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756719705Satune Solving Time: 0.033227
+ [java] Path Solving Time: 44.30735
+ [java] PetriNet for path length: 7 [places: 509 ; transitions: 2697 ; edges: 7171]
+ [java] Path Solving Time: 13.264452
+ [java] Path Solving Time: 2.968597
+ [java] 1594756722333 Original Encoding Solving Time: 0.332047
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756722333Satune Solving Time: 49.305589
+ [java] 1594756722400 Original Encoding Solving Time: 0.022812
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756722400Satune Solving Time: 0.089449
+ [java] Path Solving Time: 9.867113
+ [java] Path Solving Time: 3.081179
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756722458 Original Encoding Solving Time: 0.735661
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756722458Satune Solving Time: 47.692088
+ [java] 1594756722521 Original Encoding Solving Time: 0.022261
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756722521Satune Solving Time: 0.074247
+ [java] Path Solving Time: 8.976784
+ [java] Path Solving Time: 2.91247
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594756722581 Original Encoding Solving Time: 0.463695
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756722581Satune Solving Time: 46.958253
+ [java] 1594756722644 Original Encoding Solving Time: 0.025762
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756722644Satune Solving Time: 0.077551
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 8.542404
+ [java] Path Solving Time: 2.907071
+ [java] 1594756722699 Original Encoding Solving Time: 0.277022
+ [java] Clauses = 8 #Vars = 5
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.041686
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.041827
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb189e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb188e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb18960....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb18860....
+ [java] Encoding Graph Time: 0.000050
+ [java] Elapse Encode time: 0.000073
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 9 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.041328
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.041406
+ [java] Elapse Encode time: 0.000021
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000030
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb316a0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb31230....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb31620....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb187e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb315a0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cab6260....
+ [java] Encoding Graph Time: 0.000090
+ [java] Elapse Encode time: 0.000124
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.049167
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.049298
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000085
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000047
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb187e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb2d850....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb31230....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb316a0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb31620....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb2d970....
+ [java] Encoding Graph Time: 0.000082
+ [java] Elapse Encode time: 0.000145
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047533
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047684
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 18 #Vars = 11
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000034
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000070
+ [java] Polarity time: 0.000004
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb187e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb31620....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb31230....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b490....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b950....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b5b0....
+ [java] Encoding Graph Time: 0.000091
+ [java] Elapse Encode time: 0.000118
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046826
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046950
+ [java] Elapse Encode time: 0.000024
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000038
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000073
+ [java] PolaisSat= true ,SatuneSat= true
+ [java] 1594756722699Satune Solving Time: 47.355517
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594756722762 Original Encoding Solving Time: 0.025347
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756722762Satune Solving Time: 0.083139
+ [java] Path Solving Time: 8.810597
+ [java] Path Solving Time: 3.319005
+ [java] 1594756722818 Original Encoding Solving Time: 0.409319
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756722818Satune Solving Time: 48.331553
+ [java] 1594756722890 Original Encoding Solving Time: 0.032608
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756722890Satune Solving Time: 0.339161
+ [java] Path Solving Time: 15.464034
+ [java] Path Solving Time: 3.72972
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594756722953 Original Encoding Solving Time: 0.472396
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756722953Satune Solving Time: 49.096268
+ [java] 1594756723019 Original Encoding Solving Time: 0.02307
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723019Satune Solving Time: 0.092413
+ [java] Path Solving Time: 9.578869
+ [java] Path Solving Time: 3.355046
+ [java] 1594756723076 Original Encoding Solving Time: 0.556056
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756723076Satune Solving Time: 47.068534
+ [java] 1594756723139 Original Encoding Solving Time: 0.024847
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723139Satune Solving Time: 0.090132
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 10.425126
+ [java] Path Solving Time: 3.544775
+ [java] 1594756723197 Original Encoding Solving Time: 0.30883
+ [java] rity time: 0.000004
+ [java] Preprocess time: 0.000012
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3dea0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb2df10....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b9d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3d960....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3de20....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3da80....
+ [java] Encoding Graph Time: 0.000069
+ [java] Elapse Encode time: 0.000101
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047239
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047347
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b950....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b9d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb2df10....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3ff80....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb2df90....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb400a0....
+ [java] Encoding Graph Time: 0.000072
+ [java] Elapse Encode time: 0.000097
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.048220
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.048323
+ [java] Elapse Encode time: 0.000034
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000286
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000333
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3b9d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb40440....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb3d960....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42b40....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42680....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb427a0....
+ [java] Encoding Graph Time: 0.000131
+ [java] Elapse Encode time: 0.000171
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 22 #Vars = 13
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.048909
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.049087
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 23 #Vars = 13
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000088
+ [java] Polarity time: 0.000014
+ [java] Preprocess time: 0.000016
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb404c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb454c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42bc0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb47150....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb45000....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb45120....
+ [java] Encoding Graph Time: 0.000165
+ [java] Elapse Encode time: 0.000229
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 22 #Vars = 13
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046819
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047058
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 23 #Vars = 13
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000046
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000086
+ [java] Polarity timisSat= true ,SatuneSat= true
+ [java] 1594756723197Satune Solving Time: 47.229336
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] 1594756723261 Original Encoding Solving Time: 0.023109
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723261Satune Solving Time: 0.08595
+ [java] Path Solving Time: 15.183968
+ [java] Path Solving Time: 16.175014
+ [java] Path Solving Time: 3.339516
+ [java] 1594756723340 Original Encoding Solving Time: 0.374965
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756723340Satune Solving Time: 46.980101
+ [java] 1594756723403 Original Encoding Solving Time: 0.025349
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723403Satune Solving Time: 0.088934
+ [java] Path Solving Time: 64.83098
+ [java] Path Solving Time: 21.572358
+ [java] Path Solving Time: 30.385997
+ [java] Path Solving Time: 3.57687
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] 1594756723572 Original Encoding Solving Time: 0.441717
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756723572Satune Solving Time: 48.531137
+ [java] 1594756723636 Original Encoding Solving Time: 0.02538
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723636Satune Solving Time: 0.082771
+ [java] Done with finding holes : Flag = true
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 22.650557
+ [java] Path Solving Time: 15.958472
+ [java] Path Solving Time: 3.66011
+ [java] 1594756723722 Original Encoding Solving Time: 0.447077
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: SelectorMapping is not public in StyleSheet; cannot be accessed from outside package
+ [java] javax.swing.text.html.StyleSheet.SelectorMapping sypet_var136 = new javax.swing.text.html.StyleSheet.SelectorMapping(sypet_arg1);int sypet_var137 = sypet_var136.getSpecificity();javax.swing.text.Element sypet_var138 = sypet_arg0.getDefaultRootElement();javax.swing.text.Element sypet_var139 = sypet_var138.getElement(sypet_var137);return sypet_var139;}
+ [java] ^
+ [java] /Source.java:3: error: SelectorMapping is not public in StyleSheet; cannot be accessed from outside package
+ [java] javax.swing.text.html.StyleSheet.SelectorMapping sypet_var136 = new javax.swing.text.html.StyleSheet.SelectorMapping(sypet_arg1);int sypet_var137 = sypet_var136.getSpecificity();javax.swing.text.Element sypet_var138 = sypet_arg0.getDefaultRootElement();javax.swing.text.Element sypet_var139 = sypet_var138.getElement(sypet_var137);return sypet_var139;}
+ [java] ^
+ [java] 2 errors
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756723722Satune Solving Time: 47.605871
+ [java] 1594756723784 Original Encoding Solving Time: 0.025796
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723784Satune Solving Time: 0.093799
+ [java] Path Solving Time: 19.000764
+ [java] Path Solving Time: 21.364424
+ [java] Path Solving Time: 3.490435
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] 1594756723871 Original Encoding Solving Time: 0.353741
+ [java] e: 0.000006
+ [java] Preprocess time: 0.000013
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb404c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb46c30....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42b40....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b9df0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b9d70....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb46d50....
+ [java] Encoding Graph Time: 0.000084
+ [java] Elapse Encode time: 0.000117
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 22 #Vars = 13
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047098
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047221
+ [java] Elapse Encode time: 0.000030
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 23 #Vars = 13
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000081
+ [java] Polarity time: 0.000007
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb404c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42b40....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca094b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca09430....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca08ff0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb476b0....
+ [java] Encoding Graph Time: 0.000110
+ [java] Elapse Encode time: 0.000137
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.046829
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.046972
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000047
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000084
+ [java] Polarity time: 0.000013
+ [java] Preprocess time: 0.000022
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42b40....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb404c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb40440....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b6ca0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3ba410....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b68f0....
+ [java] Encoding Graph Time: 0.000162
+ [java] Elapse Encode time: 0.000217
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.048296
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.048520
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000043
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000079
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b31b0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb42b40....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb404c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5ca098d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b3130....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3b2d90....
+ [java] Encoding Graph Time: 0.000097
+ [java] Elapse Encode time: 0.000123
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047469
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047598
+ [java] Elapse Encode time: 0.000029
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000089
+ [java] Polarity time: 0.00000isSat= true ,SatuneSat= true
+ [java] 1594756723871Satune Solving Time: 47.365887
+ [java] 1594756723931 Original Encoding Solving Time: 0.02331
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756723931Satune Solving Time: 0.08183
+ [java] /Source.java:3: error: View is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var142 = sypet_arg0.getDefaultRootElement();javax.swing.text.Element sypet_var143 = sypet_var142.getElement(sypet_arg1);javax.swing.text.View sypet_var144 = new javax.swing.text.View(sypet_var143);javax.swing.text.Element sypet_var145 = sypet_var144.getElement();return sypet_var145;}
+ [java] ^
+ [java] 1 error
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 36.277184
+ [java] Path Solving Time: 14.785682
+ [java] Path Solving Time: 20.393228
+ [java] Path Solving Time: 3.403578
+ [java] 1594756724050 Original Encoding Solving Time: 0.307819
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: CompositeView is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var148 = sypet_arg0.getDefaultRootElement();javax.swing.text.CompositeView sypet_var149 = new javax.swing.text.CompositeView(sypet_var148);javax.swing.text.View sypet_var150 = sypet_var149.getView(sypet_arg1);javax.swing.text.Element sypet_var151 = sypet_var150.getElement();return sypet_var151;}
+ [java] ^
+ [java] 1 error
+ [java] Done with finding holes : Flag = false
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756724050Satune Solving Time: 47.890863
+ [java] 1594756724110 Original Encoding Solving Time: 0.0178
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756724110Satune Solving Time: 0.036352
+ [java] Path Solving Time: 17.755354
+ [java] Path Solving Time: 11.859444
+ [java] Path Solving Time: 3.393604
+ [java] 1594756724186 Original Encoding Solving Time: 0.339748
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756724186Satune Solving Time: 47.860368
+ [java] 1594756724246 Original Encoding Solving Time: 0.023131
+ [java] isSat= false ,SatuneSat= false
+ [java] 1594756724246Satune Solving Time: 0.089516
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] /Source.java:3: error: View is abstract; cannot be instantiated
+ [java] javax.swing.text.Element sypet_var154 = sypet_arg0.getDefaultRootElement();javax.swing.text.View sypet_var155 = new javax.swing.text.View(sypet_var154);javax.swing.text.View sypet_var156 = sypet_var155.getView(sypet_arg1);javax.swing.text.Element sypet_var157 = sypet_var156.getElement();return sypet_var157;}
+ [java] ^
+ [java] 1 error
+ [java] assumption size = 0
+ [java] Conflict Array:
+ [java] ***********************
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = false
+ [java] Path Solving Time: 20.851904
+ [java] Path Solving Time: 17.394992
+ [java] Path Solving Time: 21.145977
+ [java] 1594756724349 Original Encoding Solving Time: 0.272848
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] isSat= true ,SatuneSat= true
+ [java] 1594756724349Satune Solving Time: 47.239623
+ [java] Path Solving Time: 21.437873
+ [java] Path Solving Time: 14.400672
+ [java] Path Solving Time: 7.527637
+ [java] 1594756724498 Original Encoding Solving Time: 0.415559
+ [java] 5
+ [java] Preprocess time: 0.000015
+ [java] Decompose Order: 0.000005
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1d4c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1d3c0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1d440....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1cfa0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb40440....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1d340....
+ [java] Encoding Graph Time: 0.000081
+ [java] Elapse Encode time: 0.000116
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 16 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047236
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047358
+ [java] Elapse Encode time: 0.000028
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 17 #Vars = 10
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000041
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000077
+ [java] Polarity time: 0.000006
+ [java] Preprocess time: 0.000009
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1f550....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1f060....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1f4d0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1f0e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1eec0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1efe0....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000105
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 8
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047772
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047883
+ [java] Elapse Encode time: 0.000023
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 8
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000000
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000032
+ [java] Polarity time: 0.000005
+ [java] Preprocess time: 0.000008
+ [java] Decompose Order: 0.000003
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb21370....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb211f0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb212f0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb21270....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb21170....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb20b60....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000106
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 14 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047740
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047852
+ [java] Elapse Encode time: 0.000027
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 15 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.000049
+ [java] Result Computed in SAT solver: UNSAT
+ [java] CSOLVER solve time: 0.000085
+ [java] Polarity time: 0.000003
+ [java] Preprocess time: 0.000010
+ [java] Decompose Order: 0.000002
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb23310....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb23390....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb23290....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1a430....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb23210....
+ [java] Encoding Graph Time: 0.000079
+ [java] Elapse Encode time: 0.000104
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 10 #Vars = 6
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047122
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.047232
+ [java] Setting UNSAT %%%
+ [java] Polarity time: 0.000008
+ [java] Preprocess time: 0.000011
+ [java] Decompose Order: 0.000004
+ [java] INFO: naive encoder is making the decision about element 0x7fec5cb1ee50....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c393500....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c393390....
+ [java] INFO: naive encoder is making the decisiisSat= true ,SatuneSat= true
+ [java] 1594756724498Satune Solving Time: 48.087479
+ [java] Let's read clauses ...
+ [java] Let's read clauses ...
+ [java] Done with finding holes : Flag = true
+ [java] =========Statistics (time in milliseconds)=========
+ [java] Benchmark Id: 24
+ [java] Sketch Generation Time: 1482.8933850000003
+ [java] Sketch Completion Time: 2743.402258000001
+ [java] Compilation Time: 961.2151140000001
+ [java] Running Test cases Time: 2592.83579
+ [java] Synthesis Time: 6819.131433000001
+ [java] Total Time: 7780.346547000001
+ [java] Number of components: 4
+ [java] Number of holes: 6
+ [java] Number of completed programs: 61
+ [java] Number of sketches: 31
+ [java] Solution:
+ [java] javax.swing.text.Element sypet_var166 = sypet_arg0.getDefaultRootElement();
+ [java] int sypet_var167 = sypet_var166.getElementIndex(sypet_arg1);
+ [java] javax.swing.text.Element sypet_var168 = sypet_var166.getElement(sypet_var167);
+ [java] return sypet_var168;
+ [java]
+ [java] ============================
+ [java] on about element 0x7fec5c393670....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c3937e0....
+ [java] INFO: naive encoder is making the decision about element 0x7fec5c393950....
+ [java] Encoding Graph Time: 0.000108
+ [java] Elapse Encode time: 0.000148
+ [java] Is problem UNSAT after encoding: 0
+ [java] #Clauses = 13 #Vars = 9
+ [java] Data is available now.
+ [java] CNF Encode time: 0.000000
+ [java] SAT Solving time: 0.047911
+ [java] Result Computed in SAT solver: SAT
+ [java] CSOLVER solve time: 0.048070
+
+BUILD SUCCESSFUL
+Total time: 22 seconds
projects / Benchmarks_CSolver.git / blobdiff