Open
Description
When I run the command ./Ultimate -tc config/AutomizerBpl.xml -s config/svcomp-Reach-64bit-Automizer_Bitvector.epf -i test.bpl on the below file, I get the error SMTLIBException: Parse Error: <stdin>:14.15: cannot declare or define symbol '.a'; symbols starting with . and @ are reserved in SMT-LIB:
const .a: bv32;
axiom .a == 1bv32;
procedure f() {
assert true;
}
Below is the full error message:
Ultimate: Cannot open display:
Ultimate:
GTK+ Version Check
This is Ultimate 0.1.24-91b1670
[2019-08-30 20:26:12,031 INFO L170 SettingsManager]: Resetting all preferences to default values...
[2019-08-30 20:26:12,034 INFO L174 SettingsManager]: Resetting UltimateCore preferences to default values
[2019-08-30 20:26:12,059 INFO L177 SettingsManager]: Ultimate Commandline Interface provides no preferences, ignoring...
[2019-08-30 20:26:12,060 INFO L174 SettingsManager]: Resetting Boogie Preprocessor preferences to default values
[2019-08-30 20:26:12,067 INFO L174 SettingsManager]: Resetting Boogie Procedure Inliner preferences to default values
[2019-08-30 20:26:12,075 INFO L174 SettingsManager]: Resetting Abstract Interpretation preferences to default values
[2019-08-30 20:26:12,082 INFO L174 SettingsManager]: Resetting LassoRanker preferences to default values
[2019-08-30 20:26:12,090 INFO L174 SettingsManager]: Resetting Reaching Definitions preferences to default values
[2019-08-30 20:26:12,096 INFO L174 SettingsManager]: Resetting SyntaxChecker preferences to default values
[2019-08-30 20:26:12,101 INFO L177 SettingsManager]: Büchi Program Product provides no preferences, ignoring...
[2019-08-30 20:26:12,102 INFO L174 SettingsManager]: Resetting LTL2Aut preferences to default values
[2019-08-30 20:26:12,109 INFO L174 SettingsManager]: Resetting PEA to Boogie preferences to default values
[2019-08-30 20:26:12,114 INFO L174 SettingsManager]: Resetting BlockEncodingV2 preferences to default values
[2019-08-30 20:26:12,122 INFO L174 SettingsManager]: Resetting ChcToBoogie preferences to default values
[2019-08-30 20:26:12,130 INFO L174 SettingsManager]: Resetting AutomataScriptInterpreter preferences to default values
[2019-08-30 20:26:12,139 INFO L174 SettingsManager]: Resetting BuchiAutomizer preferences to default values
[2019-08-30 20:26:12,150 INFO L174 SettingsManager]: Resetting CACSL2BoogieTranslator preferences to default values
[2019-08-30 20:26:12,160 INFO L174 SettingsManager]: Resetting CodeCheck preferences to default values
[2019-08-30 20:26:12,171 INFO L174 SettingsManager]: Resetting InvariantSynthesis preferences to default values
[2019-08-30 20:26:12,179 INFO L174 SettingsManager]: Resetting RCFGBuilder preferences to default values
[2019-08-30 20:26:12,186 INFO L174 SettingsManager]: Resetting TraceAbstraction preferences to default values
[2019-08-30 20:26:12,195 INFO L177 SettingsManager]: TraceAbstractionConcurrent provides no preferences, ignoring...
[2019-08-30 20:26:12,195 INFO L177 SettingsManager]: TraceAbstractionWithAFAs provides no preferences, ignoring...
[2019-08-30 20:26:12,196 INFO L174 SettingsManager]: Resetting TreeAutomizer preferences to default values
[2019-08-30 20:26:12,210 INFO L174 SettingsManager]: Resetting IcfgTransformer preferences to default values
[2019-08-30 20:26:12,217 INFO L174 SettingsManager]: Resetting Boogie Printer preferences to default values
[2019-08-30 20:26:12,224 INFO L174 SettingsManager]: Resetting ReqPrinter preferences to default values
[2019-08-30 20:26:12,231 INFO L174 SettingsManager]: Resetting Witness Printer preferences to default values
[2019-08-30 20:26:12,239 INFO L177 SettingsManager]: Boogie PL CUP Parser provides no preferences, ignoring...
[2019-08-30 20:26:12,240 INFO L174 SettingsManager]: Resetting CDTParser preferences to default values
[2019-08-30 20:26:12,247 INFO L177 SettingsManager]: AutomataScriptParser provides no preferences, ignoring...
[2019-08-30 20:26:12,247 INFO L177 SettingsManager]: ReqParser provides no preferences, ignoring...
[2019-08-30 20:26:12,249 INFO L174 SettingsManager]: Resetting SmtParser preferences to default values
[2019-08-30 20:26:12,256 INFO L174 SettingsManager]: Resetting Witness Parser preferences to default values
[2019-08-30 20:26:12,262 INFO L181 SettingsManager]: Finished resetting all preferences to default values...
[2019-08-30 20:26:12,263 INFO L98 SettingsManager]: Beginning loading settings from /home/liam/uautomizer/config/svcomp-Reach-64bit-Automizer_Bitvector.epf
[2019-08-30 20:26:12,300 INFO L110 SettingsManager]: Loading preferences was successful
[2019-08-30 20:26:12,301 INFO L112 SettingsManager]: Preferences different from defaults after loading the file:
[2019-08-30 20:26:12,303 INFO L131 SettingsManager]: Preferences of Boogie Procedure Inliner differ from their defaults:
[2019-08-30 20:26:12,304 INFO L133 SettingsManager]: * ... calls to implemented procedures=ONLY_FOR_CONCURRENT_PROGRAMS
[2019-08-30 20:26:12,306 INFO L131 SettingsManager]: Preferences of BlockEncodingV2 differ from their defaults:
[2019-08-30 20:26:12,306 INFO L133 SettingsManager]: * Create parallel compositions if possible=false
[2019-08-30 20:26:12,307 INFO L133 SettingsManager]: * Use SBE=true
[2019-08-30 20:26:12,308 INFO L131 SettingsManager]: Preferences of CACSL2BoogieTranslator differ from their defaults:
[2019-08-30 20:26:12,309 INFO L133 SettingsManager]: * Check division by zero=IGNORE
[2019-08-30 20:26:12,314 INFO L133 SettingsManager]: * Pointer to allocated memory at dereference=IGNORE
[2019-08-30 20:26:12,321 INFO L133 SettingsManager]: * If two pointers are subtracted or compared they have the same base address=IGNORE
[2019-08-30 20:26:12,322 INFO L133 SettingsManager]: * Check array bounds for arrays that are off heap=IGNORE
[2019-08-30 20:26:12,322 INFO L133 SettingsManager]: * Use bitvectors instead of ints=true
[2019-08-30 20:26:12,323 INFO L133 SettingsManager]: * Memory model=HoenickeLindenmann_4ByteResolution
[2019-08-30 20:26:12,324 INFO L133 SettingsManager]: * Check if freed pointer was valid=false
[2019-08-30 20:26:12,325 INFO L133 SettingsManager]: * Use constant arrays=true
[2019-08-30 20:26:12,330 INFO L133 SettingsManager]: * Pointer base address is valid at dereference=IGNORE
[2019-08-30 20:26:12,337 INFO L131 SettingsManager]: Preferences of RCFGBuilder differ from their defaults:
[2019-08-30 20:26:12,338 INFO L133 SettingsManager]: * Size of a code block=SequenceOfStatements
[2019-08-30 20:26:12,339 INFO L133 SettingsManager]: * To the following directory=./dump/
[2019-08-30 20:26:12,340 INFO L133 SettingsManager]: * SMT solver=External_DefaultMode
[2019-08-30 20:26:12,340 INFO L133 SettingsManager]: * Command for external solver=z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2019-08-30 20:26:12,344 INFO L131 SettingsManager]: Preferences of TraceAbstraction differ from their defaults:
[2019-08-30 20:26:12,352 INFO L133 SettingsManager]: * Compute Interpolants along a Counterexample=FPandBP
[2019-08-30 20:26:12,353 INFO L133 SettingsManager]: * Positions where we compute the Hoare Annotation=LoopsAndPotentialCycles
[2019-08-30 20:26:12,354 INFO L133 SettingsManager]: * Trace refinement strategy=WOLF
[2019-08-30 20:26:12,355 INFO L133 SettingsManager]: * SMT solver=External_ModelsAndUnsatCoreMode
[2019-08-30 20:26:12,355 INFO L133 SettingsManager]: * Command for external solver=cvc4 --incremental --rewrite-divk --print-success --lang smt
[2019-08-30 20:26:12,356 INFO L133 SettingsManager]: * Logic for external solver=AUFBV
[2019-08-30 20:26:12,360 INFO L133 SettingsManager]: * Compute Hoare Annotation of negated interpolant automaton, abstraction and CFG=true
[2019-08-30 20:26:12,366 INFO L133 SettingsManager]: * To the following directory=dump/
[2019-08-30 20:26:12,405 INFO L81 nceAwareModelManager]: Repository-Root is: /tmp
[2019-08-30 20:26:12,426 INFO L258 ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2019-08-30 20:26:12,432 INFO L214 ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2019-08-30 20:26:12,436 INFO L271 PluginConnector]: Initializing Boogie PL CUP Parser...
[2019-08-30 20:26:12,438 INFO L276 PluginConnector]: Boogie PL CUP Parser initialized
[2019-08-30 20:26:12,442 INFO L418 ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /home/liam/uautomizer/test.bpl
[2019-08-30 20:26:12,443 INFO L111 BoogieParser]: Parsing: '/home/liam/uautomizer/test.bpl'
[2019-08-30 20:26:12,494 INFO L296 ainManager$Toolchain]: ####################### [Toolchain 1] #######################
[2019-08-30 20:26:12,498 INFO L131 ToolchainWalker]: Walking toolchain with 3 elements.
[2019-08-30 20:26:12,499 INFO L113 PluginConnector]: ------------------------Boogie Preprocessor----------------------------
[2019-08-30 20:26:12,500 INFO L271 PluginConnector]: Initializing Boogie Preprocessor...
[2019-08-30 20:26:12,501 INFO L276 PluginConnector]: Boogie Preprocessor initialized
[2019-08-30 20:26:12,538 INFO L185 PluginConnector]: Executing the observer EnsureBoogieModelObserver from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,545 INFO L185 PluginConnector]: Executing the observer TypeChecker from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,561 INFO L185 PluginConnector]: Executing the observer ConstExpander from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,563 INFO L185 PluginConnector]: Executing the observer StructExpander from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,575 INFO L185 PluginConnector]: Executing the observer UnstructureCode from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,578 INFO L185 PluginConnector]: Executing the observer FunctionInliner from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,582 INFO L185 PluginConnector]: Executing the observer BoogieSymbolTableConstructor from plugin Boogie Preprocessor for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
[2019-08-30 20:26:12,589 INFO L132 PluginConnector]: ------------------------ END Boogie Preprocessor----------------------------
[2019-08-30 20:26:12,591 INFO L113 PluginConnector]: ------------------------RCFGBuilder----------------------------
[2019-08-30 20:26:12,592 INFO L271 PluginConnector]: Initializing RCFGBuilder...
[2019-08-30 20:26:12,593 INFO L276 PluginConnector]: RCFGBuilder initialized
[2019-08-30 20:26:12,595 INFO L185 PluginConnector]: Executing the observer RCFGBuilderObserver from plugin RCFGBuilder for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/1) ...
No working directory specified, using /home/liam/uautomizer/z3
Starting monitored process 1 with z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000 (exit command is (exit), workingDir is null)
Waiting until toolchain timeout for monitored process 1 with z3 SMTLIB2_COMPLIANT=true -memory:2024 -smt2 -in -t:2000
[2019-08-30 20:26:12,703 INFO L124 BoogieDeclarations]: Specification and implementation of procedure f given in one single declaration
[2019-08-30 20:26:12,704 INFO L130 BoogieDeclarations]: Found specification of procedure f
[2019-08-30 20:26:12,705 INFO L138 BoogieDeclarations]: Found implementation of procedure f
[2019-08-30 20:26:12,837 INFO L272 CfgBuilder]: Using library mode
[2019-08-30 20:26:12,839 INFO L280 CfgBuilder]: Removed 0 assue(true) statements.
[2019-08-30 20:26:12,841 INFO L202 PluginConnector]: Adding new model test.bpl de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 30.08 08:26:12 BoogieIcfgContainer
[2019-08-30 20:26:12,842 INFO L132 PluginConnector]: ------------------------ END RCFGBuilder----------------------------
[2019-08-30 20:26:12,843 INFO L113 PluginConnector]: ------------------------TraceAbstraction----------------------------
[2019-08-30 20:26:12,844 INFO L271 PluginConnector]: Initializing TraceAbstraction...
[2019-08-30 20:26:12,847 INFO L276 PluginConnector]: TraceAbstraction initialized
[2019-08-30 20:26:12,848 INFO L185 PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "test.bpl de.uni_freiburg.informatik.ultimate.boogie.parser AST 30.08 08:26:12" (1/2) ...
[2019-08-30 20:26:12,850 INFO L205 PluginConnector]: Invalid model from TraceAbstraction for observer de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver@44415612 and model type test.bpl de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction AST 30.08 08:26:12, skipping insertion in model container
[2019-08-30 20:26:12,850 INFO L185 PluginConnector]: Executing the observer TraceAbstractionObserver from plugin TraceAbstraction for "test.bpl de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder CFG 30.08 08:26:12" (2/2) ...
[2019-08-30 20:26:12,853 INFO L112 eAbstractionObserver]: Analyzing ICFG test.bpl
[2019-08-30 20:26:12,869 INFO L156 ceAbstractionStarter]: Automizer settings: Hoare:true NWA Interpolation:FPandBP Determinization: PREDICATE_ABSTRACTION
[2019-08-30 20:26:12,880 INFO L168 ceAbstractionStarter]: Appying trace abstraction to program that has 1 error locations.
[2019-08-30 20:26:12,908 INFO L257 AbstractCegarLoop]: Starting to check reachability of 1 error locations.
[2019-08-30 20:26:12,946 INFO L133 ementStrategyFactory]: Using default assertion order modulation
[2019-08-30 20:26:12,948 INFO L382 AbstractCegarLoop]: Interprodecural is true
[2019-08-30 20:26:12,948 INFO L383 AbstractCegarLoop]: Hoare is true
[2019-08-30 20:26:12,949 INFO L384 AbstractCegarLoop]: Compute interpolants for FPandBP
[2019-08-30 20:26:12,950 INFO L385 AbstractCegarLoop]: Backedges is STRAIGHT_LINE
[2019-08-30 20:26:12,951 INFO L386 AbstractCegarLoop]: Determinization is PREDICATE_ABSTRACTION
[2019-08-30 20:26:12,951 INFO L387 AbstractCegarLoop]: Difference is false
[2019-08-30 20:26:12,952 INFO L388 AbstractCegarLoop]: Minimize is MINIMIZE_SEVPA
[2019-08-30 20:26:12,953 INFO L393 AbstractCegarLoop]: ======== Iteration 0==of CEGAR loop == AllErrorsAtOnce========
[2019-08-30 20:26:12,975 INFO L276 IsEmpty]: Start isEmpty. Operand 4 states.
[2019-08-30 20:26:12,985 INFO L282 IsEmpty]: Finished isEmpty. Found accepting run of length 2
[2019-08-30 20:26:12,985 INFO L394 BasicCegarLoop]: Found error trace
[2019-08-30 20:26:12,987 INFO L402 BasicCegarLoop]: trace histogram [1]
[2019-08-30 20:26:12,993 INFO L423 AbstractCegarLoop]: === Iteration 1 === [fErr0ASSERT_VIOLATIONASSERT]===
[2019-08-30 20:26:13,002 INFO L141 PredicateUnifier]: Initialized classic predicate unifier
[2019-08-30 20:26:13,003 INFO L82 PathProgramCache]: Analyzing trace with hash 31, now seen corresponding path program 1 times
[2019-08-30 20:26:13,008 INFO L223 ckRefinementStrategy]: Switched to mode CVC4_FPBP
[2019-08-30 20:26:13,009 INFO L69 tionRefinementEngine]: Using refinement strategy WolfRefinementStrategy
No working directory specified, using /home/liam/uautomizer/cvc4
Starting monitored process 2 with cvc4 --incremental --print-success --lang smt --rewrite-divk (exit command is (exit), workingDir is null)
Waiting until toolchain timeout for monitored process 2 with cvc4 --incremental --print-success --lang smt --rewrite-divk
[MP cvc4 --incremental --print-success --lang smt --rewrite-divk (2)] Exception during sending of exit command (exit): Broken pipe
[2019-08-30 20:26:13,264 WARN L521 AbstractCegarLoop]: Destroyed unattended storables created during the last iteration: 2 cvc4 --incremental --print-success --lang smt --rewrite-divk
[2019-08-30 20:26:13,274 FATAL L265 ToolchainWalker]: An unrecoverable error occured during an interaction with an SMT solver:
de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: Parse Error: <stdin>:14.15: cannot declare or define symbol `.a'; symbols starting with . and @ are reserved in SMT-LIB
(declare-fun .a () (_ BitVec 32))
^
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Parser$Action$.CUP$do_action(Parser.java:1420)
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Parser.do_action(Parser.java:630)
at com.github.jhoenicke.javacup.runtime.LRParser.parse(LRParser.java:419)
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.parse(Executor.java:205)
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Executor.parseSuccess(Executor.java:221)
at de.uni_freiburg.informatik.ultimate.smtsolver.external.Scriptor.declareFun(Scriptor.java:118)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.smt.TermTransferrer.convertApplicationTerm(TermTransferrer.java:163)
at de.uni_freiburg.informatik.ultimate.logic.TermTransformer$BuildApplicationTerm.walk(TermTransformer.java:320)
at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:122)
at de.uni_freiburg.informatik.ultimate.logic.NonRecursive.run(NonRecursive.java:113)
at de.uni_freiburg.informatik.ultimate.logic.TermTransformer.transform(TermTransformer.java:253)
at de.uni_freiburg.informatik.ultimate.modelcheckerutils.cfg.SmtSymbols.transferSymbols(SmtSymbols.java:129)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.MultiTrackRefinementStrategy.constructManagedScript(MultiTrackRefinementStrategy.java:419)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.MultiTrackRefinementStrategy.constructTraceCheckConstructor(MultiTrackRefinementStrategy.java:303)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.MultiTrackRefinementStrategy.getTraceCheck(MultiTrackRefinementStrategy.java:230)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.BaseRefinementStrategy.checkFeasibility(BaseRefinementStrategy.java:223)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.BaseRefinementStrategy.executeStrategy(BaseRefinementStrategy.java:197)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.tracehandling.TraceAbstractionRefinementEngine.<init>(TraceAbstractionRefinementEngine.java:70)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.BasicCegarLoop.isCounterexampleFeasible(BasicCegarLoop.java:456)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterateInternal(AbstractCegarLoop.java:434)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.AbstractCegarLoop.iterate(AbstractCegarLoop.java:376)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.iterate(TraceAbstractionStarter.java:334)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.runCegarLoops(TraceAbstractionStarter.java:174)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionStarter.<init>(TraceAbstractionStarter.java:126)
at de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.TraceAbstractionObserver.finish(TraceAbstractionObserver.java:123)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runObserver(PluginConnector.java:168)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.runTool(PluginConnector.java:151)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.PluginConnector.run(PluginConnector.java:128)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.executePluginConnector(ToolchainWalker.java:232)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.processPlugin(ToolchainWalker.java:226)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walkUnprotected(ToolchainWalker.java:142)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainWalker.walk(ToolchainWalker.java:104)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.ToolchainManager$Toolchain.processToolchain(ToolchainManager.java:316)
at de.uni_freiburg.informatik.ultimate.core.coreplugin.toolchain.DefaultToolchainJob.run(DefaultToolchainJob.java:145)
at org.eclipse.core.internal.jobs.Worker.run(Worker.java:55)
[2019-08-30 20:26:13,415 INFO L168 Benchmark]: Toolchain (without parser) took 919.17 ms. Allocated memory is still 514.9 MB. Free memory was 473.4 MB in the beginning and 453.6 MB in the end (delta: 19.8 MB). Peak memory consumption was 19.8 MB. Max. memory is 11.5 GB.
[2019-08-30 20:26:13,421 INFO L168 Benchmark]: Boogie PL CUP Parser took 0.57 ms. Allocated memory is still 514.9 MB. Free memory is still 474.9 MB. There was no memory consumed. Max. memory is 11.5 GB.
[2019-08-30 20:26:13,428 INFO L168 Benchmark]: Boogie Preprocessor took 91.72 ms. Allocated memory is still 514.9 MB. Free memory was 473.4 MB in the beginning and 472.0 MB in the end (delta: 1.3 MB). Peak memory consumption was 1.3 MB. Max. memory is 11.5 GB.
[2019-08-30 20:26:13,435 INFO L168 Benchmark]: RCFGBuilder took 251.22 ms. Allocated memory is still 514.9 MB. Free memory was 472.0 MB in the beginning and 463.1 MB in the end (delta: 8.9 MB). Peak memory consumption was 8.9 MB. Max. memory is 11.5 GB.
[2019-08-30 20:26:13,439 INFO L168 Benchmark]: TraceAbstraction took 570.12 ms. Allocated memory is still 514.9 MB. Free memory was 463.1 MB in the beginning and 453.6 MB in the end (delta: 9.5 MB). Peak memory consumption was 9.5 MB. Max. memory is 11.5 GB.
[2019-08-30 20:26:13,449 INFO L336 ainManager$Toolchain]: ####################### End [Toolchain 1] #######################
--- Results ---
* Results from de.uni_freiburg.informatik.ultimate.core:
- StatisticsResult: Toolchain Benchmarks
Benchmark results are:
* Boogie PL CUP Parser took 0.57 ms. Allocated memory is still 514.9 MB. Free memory is still 474.9 MB. There was no memory consumed. Max. memory is 11.5 GB.
* Boogie Preprocessor took 91.72 ms. Allocated memory is still 514.9 MB. Free memory was 473.4 MB in the beginning and 472.0 MB in the end (delta: 1.3 MB). Peak memory consumption was 1.3 MB. Max. memory is 11.5 GB.
* RCFGBuilder took 251.22 ms. Allocated memory is still 514.9 MB. Free memory was 472.0 MB in the beginning and 463.1 MB in the end (delta: 8.9 MB). Peak memory consumption was 8.9 MB. Max. memory is 11.5 GB.
* TraceAbstraction took 570.12 ms. Allocated memory is still 514.9 MB. Free memory was 463.1 MB in the beginning and 453.6 MB in the end (delta: 9.5 MB). Peak memory consumption was 9.5 MB. Max. memory is 11.5 GB.
* Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
- ExceptionOrErrorResult: SMTLIBException: Parse Error: <stdin>:14.15: cannot declare or define symbol `.a'; symbols starting with . and @ are reserved in SMT-LIB
(declare-fun .a () (_ BitVec 32))
^
de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction: SMTLIBException: Parse Error: <stdin>:14.15: cannot declare or define symbol `.a'; symbols starting with . and @ are reserved in SMT-LIB
(declare-fun .a () (_ BitVec 32))
^
: de.uni_freiburg.informatik.ultimate.smtsolver.external.Parser$Action$.CUP$do_action(Parser.java:1420)
RESULT: Ultimate could not prove your program: Toolchain returned no result.
Received shutdown request...
While it is true that SMT-LIB disallows symbols beginning with a period, Boogie does not. In the original paper, at the bottom of page 3 it describes what characters identifiers may consist of, and periods are listed. Would you be able to allow periods at the beginning of Boogie identifiers so that it's consistent with the Boogie specification?
By the way, if I instead run the command ./Ultimate -tc config/AutomizerBpl.xml -s config/svcomp-Reach-64bit-Automizer_Default.epf -i test2.bpl on the below file (the non-bitvector version of the original), it results in no errors:
const .a: int;
axiom .a == 1;
procedure f() {
assert true;
}