search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
194 stars 40 forks source link

Boogie variables beginning with a period are disallowed #445

Open liammachado opened 5 years ago

liammachado commented 5 years ago

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;
}
Heizmann commented 5 years ago

Thanks for reporting this. We probably have to escape an initial dot while translating identifiers from Boogie to SMT-LIB.

danieldietsch commented 5 years ago

I will have a look.

Heizmann commented 5 years ago

I had some time to think about this. We should use the quoted symbols mentioned in 3.1 of the SMT-LIB standard We can then translate .myConst into |.myConst|. A question is whether we should translate every Boogie identifier into a quoted SMT symbol or only those where we have to quote something (Is there more that has to be quoted?)

jhoenicke commented 5 years ago

The SMT-LIB standard demand that .myConst and |.myConst| are treated as the same identifier. At least this is explicitly mentioned for abc and |abc|. So quoting doesn't help.

Our library decides itself whether to print the symbol quoted or unquoted. You cannot force to quote it.

danieldietsch commented 5 years ago

For completeness sake: The SMT-LIB Standard Version 2.6, Sec 3.1, p24, Symbols, last paragraph:

Simple symbols starting with the character @ or . are reserved for solver use.^4 Solvers can use them respectively as identifiers for abstract values and solver-generated function symbols other than abstract values. ... ^4 This includes symbols such as |@abc| and |.abc| which are considered the same as @abc and .abc, respectively.

z3 allows these symbols, cvc4 does not. I did not try SMTInterpol, but Liam's example from above suggests that SMTInterpol is also ok with that.

I will rename the offending identifiers during ICFG creation, i.e., in Boogie2SmtSymbolTable.