./Dartagnan-SVCOMP.sh /mnt/goblint-svcomp/goblint-bench/bench/concrat/properties/no-data-race.prp /mnt/goblint-svcomp/goblint-bench/bench/concrat/fzy/main.c


--------------------------------------------------------------------------------


13:34:10 [INFO ] Compilation.compileWithClang - Compiling with clang
13:34:10 [INFO ] Compilation.compileWithSmack - Compiling with smack
13:34:11 [INFO ] GitInfo.CreateGitInfo - Git branch: svcomp
13:34:11 [INFO ] GitInfo.CreateGitInfo - Git commit ID: d54f8e1624095bb050a87db313b239cadadd9f19
13:34:11 [INFO ] GlobalSettings.LogGlobalSettings - ARCH_PRECISION: -1
13:34:11 [INFO ] GlobalSettings.LogGlobalSettings - ATOMIC_AS_LOCK: false
13:34:11 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_GENERATE_GRAPHVIZ_DEBUG_FILES: false
13:34:11 [INFO ] GlobalSettings.LogGlobalSettings - REFINEMENT_SYMMETRY_LEARNING: FULL
13:34:11 [INFO ] Dartagnan.main - Program path: /mnt/goblint-svcomp/benchexec/tools-pldi/dartagnan/output/main.bpl
13:34:11 [INFO ] Dartagnan.main - CAT file path: cat/svcomp.cat
13:34:13 [INFO ] VisitorBoogie.visitLine_comment - SMACK version: 2.8.0 
Exception in thread "main" com.dat3m.dartagnan.exception.ParsingException: Function $fp has no implementation
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitFun_expr(VisitorBoogie.java:711)
	at com.dat3m.dartagnan.parsers.BoogieParser$Fun_exprContext.accept(BoogieParser.java:5874)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitAtom_expr(BoogieBaseVisitor.java:499)
	at com.dat3m.dartagnan.parsers.BoogieParser$Atom_exprContext.accept(BoogieParser.java:5597)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitArray_expr(BoogieBaseVisitor.java:492)
	at com.dat3m.dartagnan.parsers.BoogieParser$Array_exprContext.accept(BoogieParser.java:5446)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitCoercion_expr(BoogieBaseVisitor.java:485)
	at com.dat3m.dartagnan.parsers.BoogieParser$Coercion_exprContext.accept(BoogieParser.java:5337)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitUnary_expr(BoogieBaseVisitor.java:457)
	at com.dat3m.dartagnan.parsers.BoogieParser$Unary_exprContext.accept(BoogieParser.java:5107)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitPower(BoogieBaseVisitor.java:450)
	at com.dat3m.dartagnan.parsers.BoogieParser$PowerContext.accept(BoogieParser.java:5038)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitFactor(VisitorBoogie.java:615)
	at com.dat3m.dartagnan.parsers.BoogieParser$FactorContext.accept(BoogieParser.java:4899)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitTerm(VisitorBoogie.java:604)
	at com.dat3m.dartagnan.parsers.BoogieParser$TermContext.accept(BoogieParser.java:4766)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitBv_term(BoogieBaseVisitor.java:415)
	at com.dat3m.dartagnan.parsers.BoogieParser$Bv_termContext.accept(BoogieParser.java:4694)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitRel_expr(VisitorBoogie.java:593)
	at com.dat3m.dartagnan.parsers.BoogieParser$Rel_exprContext.accept(BoogieParser.java:4528)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitLogical_expr(VisitorBoogie.java:545)
	at com.dat3m.dartagnan.parsers.BoogieParser$Logical_exprContext.accept(BoogieParser.java:4221)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitImplies_expr(BoogieBaseVisitor.java:359)
	at com.dat3m.dartagnan.parsers.BoogieParser$Implies_exprContext.accept(BoogieParser.java:4126)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitExpr(BoogieBaseVisitor.java:352)
	at com.dat3m.dartagnan.parsers.BoogieParser$ExprContext.accept(BoogieParser.java:4052)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitFun_expr(VisitorBoogie.java:666)
	at com.dat3m.dartagnan.parsers.BoogieParser$Fun_exprContext.accept(BoogieParser.java:5874)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitAtom_expr(BoogieBaseVisitor.java:499)
	at com.dat3m.dartagnan.parsers.BoogieParser$Atom_exprContext.accept(BoogieParser.java:5597)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitArray_expr(BoogieBaseVisitor.java:492)
	at com.dat3m.dartagnan.parsers.BoogieParser$Array_exprContext.accept(BoogieParser.java:5446)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitCoercion_expr(BoogieBaseVisitor.java:485)
	at com.dat3m.dartagnan.parsers.BoogieParser$Coercion_exprContext.accept(BoogieParser.java:5337)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitUnary_expr(BoogieBaseVisitor.java:457)
	at com.dat3m.dartagnan.parsers.BoogieParser$Unary_exprContext.accept(BoogieParser.java:5107)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitPower(BoogieBaseVisitor.java:450)
	at com.dat3m.dartagnan.parsers.BoogieParser$PowerContext.accept(BoogieParser.java:5038)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitFactor(VisitorBoogie.java:615)
	at com.dat3m.dartagnan.parsers.BoogieParser$FactorContext.accept(BoogieParser.java:4899)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitTerm(VisitorBoogie.java:604)
	at com.dat3m.dartagnan.parsers.BoogieParser$TermContext.accept(BoogieParser.java:4766)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitBv_term(BoogieBaseVisitor.java:415)
	at com.dat3m.dartagnan.parsers.BoogieParser$Bv_termContext.accept(BoogieParser.java:4694)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitRel_expr(VisitorBoogie.java:593)
	at com.dat3m.dartagnan.parsers.BoogieParser$Rel_exprContext.accept(BoogieParser.java:4528)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitLogical_expr(VisitorBoogie.java:545)
	at com.dat3m.dartagnan.parsers.BoogieParser$Logical_exprContext.accept(BoogieParser.java:4221)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitImplies_expr(BoogieBaseVisitor.java:359)
	at com.dat3m.dartagnan.parsers.BoogieParser$Implies_exprContext.accept(BoogieParser.java:4126)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitExpr(BoogieBaseVisitor.java:352)
	at com.dat3m.dartagnan.parsers.BoogieParser$ExprContext.accept(BoogieParser.java:4052)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitAssign_cmd(VisitorBoogie.java:410)
	at com.dat3m.dartagnan.parsers.BoogieParser$Assign_cmdContext.accept(BoogieParser.java:2456)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitLabel_or_cmd(BoogieBaseVisitor.java:177)
	at com.dat3m.dartagnan.parsers.BoogieParser$Label_or_cmdContext.accept(BoogieParser.java:2129)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitProc_decl(VisitorBoogie.java:281)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitCall_cmd(VisitorBoogie.java:384)
	at com.dat3m.dartagnan.parsers.BoogieParser$Call_cmdContext.accept(BoogieParser.java:2752)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitLabel_or_cmd(BoogieBaseVisitor.java:177)
	at com.dat3m.dartagnan.parsers.BoogieParser$Label_or_cmdContext.accept(BoogieParser.java:2129)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitProc_decl(VisitorBoogie.java:281)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitCall_cmd(VisitorBoogie.java:384)
	at com.dat3m.dartagnan.parsers.BoogieParser$Call_cmdContext.accept(BoogieParser.java:2752)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.BoogieBaseVisitor.visitLabel_or_cmd(BoogieBaseVisitor.java:177)
	at com.dat3m.dartagnan.parsers.BoogieParser$Label_or_cmdContext.accept(BoogieParser.java:2129)
	at org.antlr.v4.runtime.tree.AbstractParseTreeVisitor.visitChildren(AbstractParseTreeVisitor.java:46)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitProc_decl(VisitorBoogie.java:281)
	at com.dat3m.dartagnan.parsers.program.visitors.boogie.VisitorBoogie.visitMain(VisitorBoogie.java:131)
	at com.dat3m.dartagnan.parsers.BoogieParser$MainContext.accept(BoogieParser.java:235)
	at com.dat3m.dartagnan.parsers.program.ParserBoogie.parse(ParserBoogie.java:26)
	at com.dat3m.dartagnan.parsers.program.ProgramParser.parse(ProgramParser.java:35)
	at com.dat3m.dartagnan.Dartagnan.main(Dartagnan.java:97)
