crestdsl / CREST

Continuous REactive SysTems DSL
https://crestdsl.github.io
MIT License
18 stars 2 forks source link

z3-variable Creation Issue #16

Open gmarthe opened 5 years ago

gmarthe commented 5 years ago

There is an issue in the "ElectricPart" cell of the ErrElectric file that we didn't understand when we looked at it two weeks ago. It says there is 2 mistakes, but the first one is "'Sun' object has no attribute 'light'", whereas there is nowhere I've written Sun.light. I don't really understand the second one otherwise, "I do not know how to create a z3-variable for type None (name: light_139788611166952-else_0_139788613701024)" isn't an easy explanation to debug easily.

The ErrLiving file and the ones to run it can be found in the LivingRoomError.zip

ElectricPartError.zip