SpoonLabs / nopol

Automatic program repair system for Java based on dynamic analysis and code synthesis with SMT. Also contains the code of Dynamoth.
https://hal.archives-ouvertes.fr/hal-01285008/document
GNU General Public License v2.0
97 stars 40 forks source link

program was excuted successfully but there was NO SYNTHESIS #191

Closed qq956916631 closed 5 years ago

qq956916631 commented 5 years ago

I have tested many cases, but all of them are like this, I can't find the reason, I hope to get help, thank you so much

00:19:01.930 [pool-2-thread-1] DEBUG f.i.l.c.s.ConstraintBasedSynthesis - Failed code synthesis, returning NullCodeGenesis 00:19:01.933 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - ----INFORMATION---- 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb classes : 32 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb methods : 54 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb Statements Analyzed : 1 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb Statements with Angelic Value Found : 1 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb inputs in SMT : 0 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb SMT level: 5 00:19:01.978 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb SMT components: [14] [== of arity: 2, != of arity: 2, < of arity: 2, <= of arity: 2, ! of arity: 1, || of arity: 2, && of arity: 2, == of arity: 2, != of arity: 2, < of arity: 2, <= of arity: 2, ! of arity: 1, || of arity: 2, && of arity: 2] 00:19:01.979 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - class java.lang.Boolean: 14 00:19:01.979 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - Nb variables in SMT : 0 00:19:01.979 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - NoPol Execution time : 4341ms 00:19:01.979 [pool-1-thread-1] INFO fr.inria.lille.repair.nopol.NoPol - NO_SYNTHESIS

qq956916631 commented 5 years ago

I only test the example in "test-projects",but I also get "NO_SYNTHESIS"

qq956916631 commented 5 years ago

I found the root cause of the problem, which is that my Z3 is not working normally.

monperrus commented 5 years ago

Great, thanks for the follow up