Compilation with `SMTChecker` fails

[elenadimitrova]

Issue

Compilation with SMTChecker fails with InternalCompilerError

Steps to Reproduce

1. Build custom solc with Z3 support Note that installing Z3 for me wasn't exactly straight forward, so I've recorded the steps in point 1 here https://github.com/JoinColony/colonyNetwork/issues/547

2. Switch the truffle compiler to use this

   compilers: {
   solc: {
     version: "native"
   }
   }

3. Add pragma experimental "SMTChecker"; to a single contract.

4. Run truffle compile

Expected Behavior

Contract compiles successfully

Actual Results

$ /Users/Elena/colonyNetwork/node_modules/.bin/truffle compile

Compiling your contracts...
===========================
> Compiling ./contracts/Colony.sol
> Compiling ./contracts/ColonyFunding.sol
> Compiling ./contracts/ColonyPayment.sol
> Compiling ./contracts/ColonyStorage.sol
> Compiling ./contracts/ColonyTask.sol
> Compiling ./contracts/PatriciaTree/Data.sol
> Compiling ./contracts/PatriciaTree/IPatriciaTree.sol
> Compiling ./contracts/PatriciaTree/IPatriciaTreeBase.sol
> Compiling ./contracts/PatriciaTree/IPatriciaTreeNoHash.sol
> Compiling ./contracts/PatriciaTree/PatriciaTree.sol
> Compiling ./contracts/PatriciaTree/PatriciaTreeBase.sol
> Compiling ./contracts/PatriciaTree/PatriciaTreeNoHash.sol
> Compiling ./contracts/PatriciaTree/PatriciaTreeProofs.sol
> Compiling ./contracts/ReputationMiningCycle.sol
> Compiling ./contracts/ReputationMiningCycleRespond.sol
> Compiling ./contracts/testHelpers/FunctionsNotAvailableOnColony.sol
> Compiling ./contracts/testHelpers/NoLimitSubdomains.sol
> Compiling ./contracts/testHelpers/TaskSkillEditing.sol

InternalCompilerError:

Compilation failed. See above.
Truffle v5.0.18 (core: 5.0.18)
Node v10.13.0
error Command failed with exit code 1.

Environment

• Operating System: OSX
• Ethereum client: ganache-cli
• Truffle version (truffle version): 5.0.18
• node version (node --version): 10.12.0
• npm version (npm --version): 6.4.1

[CruzMolina]

@elenadimitrova are you able to successfully compile your contracts using the custom solc outside of truffle?

InternalCompilerError looks like a solc compiler specific error.

Edit: See item 9.

[elenadimitrova]

Yes indeed. I logged it separately, see above. It'll be nice that we actually get the compiler internal output on error with truffle as reproducing it with solc itself is not always as straight forward. For example when running solc --allow-paths I have not found a way to do this sort of thing with the path truffle compile --contracts_directory 'lib/dappsys/[!note][!stop][!proxy][!thing][!token]*.sol'

[fxfactorial]

Ping - has there been any update to this - would be great if it was straight forward as in truffle config the solc.version could accept something like 0.6.12+z3 or something like that

[eggplantzzz]

I'm not sure there has been any activity on this yet. Are you saying you want to configure your own version of solc? You can indeed do that kind of thing - you can specify a path to a local solc, a docker image, whaterver solc is installed natively, or any version you can find when doing truffle compile --list. I don't know if this is helpful but here are the compiler config docs https://www.trufflesuite.com/docs/truffle/reference/configuration#solc

[fxfactorial]

ya - something like that - like so that truffle could compile with the version of solidity that was built with smt checking enabled

will check that doc -