Record literals not type-checking properly

[noloerino]

In some situations, instantiating a record with tuple literal syntax (mentioned as a possible workaround in #99) causes runtime errors. I've found two separate errors (plus a third that I can't seem to reproduce), but I'm grouping them in one issue since I would imagine they have a similar root cause.

Issue 1

Reading properties of variables initialized with record syntax results in java.util.NoSuchElementException: None.get.

Minimal example

module main {
    type rec_t = record { f1 : integer, f2 : bv32 };

    var state : rec_t;

    init {
        state = { 100, 100bv32 };
    }   

    next {
        assert (state.f1 != 200);
    }   

    control {
        bmc_noLTL(5);
        check
    }   
}

Running this on latest master (e244310) produces the following stack trace:

Exception in thread "main" java.util.NoSuchElementException: None.get
	at scala.None$.get(Option.scala:529)
	at scala.None$.get(Option.scala:527)
	at uclid.smt.RecordSelectOp.resultType(SMTLanguage.scala:622)
	at uclid.smt.OperatorApplication.<init>(SMTLanguage.scala:849)
	at uclid.smt.Converter$._exprToSMT(Converter.scala:288)
	at uclid.smt.Converter$.toSMT$1(Converter.scala:248)
	at uclid.smt.Converter$.$anonfun$_exprToSMT$1(Converter.scala:249)
	at scala.collection.immutable.List.map(List.scala:286)
	at uclid.smt.Converter$.toSMTs$1(Converter.scala:249)
	at uclid.smt.Converter$._exprToSMT(Converter.scala:287)
	at uclid.smt.Converter$.exprToSMT(Converter.scala:319)
	at uclid.SymbolicSimulator.evaluate(SymbolicSimulator.scala:1804)
	at uclid.SymbolicSimulator.simulateStmt(SymbolicSimulator.scala:1660)
	at uclid.SymbolicSimulator.$anonfun$simulateStmt$1(SymbolicSimulator.scala:1592)
	at scala.collection.LinearSeqOptimized.foldLeft(LinearSeqOptimized.scala:126)
	at scala.collection.LinearSeqOptimized.foldLeft$(LinearSeqOptimized.scala:122)
	at scala.collection.immutable.List.foldLeft(List.scala:89)
	at uclid.SymbolicSimulator.simulateStmtList$1(SymbolicSimulator.scala:1592)
	at uclid.SymbolicSimulator.simulateStmt(SymbolicSimulator.scala:1715)
	at uclid.SymbolicSimulator.simulateModuleNext(SymbolicSimulator.scala:1582)
	at uclid.SymbolicSimulator.$anonfun$symbolicSimulate$1(SymbolicSimulator.scala:1124)
	at scala.collection.immutable.Range.foreach$mVc$sp(Range.scala:158)
	at uclid.SymbolicSimulator.symbolicSimulate(SymbolicSimulator.scala:1120)
	at uclid.SymbolicSimulator.prove$1(SymbolicSimulator.scala:228)
	at uclid.SymbolicSimulator.$anonfun$execute$6(SymbolicSimulator.scala:246)
	at uclid.SymbolicSimulator.$anonfun$execute$6$adapted(SymbolicSimulator.scala:236)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.SymbolicSimulator.execute(SymbolicSimulator.scala:236)
	at uclid.UclidMain$.execute(UclidMain.scala:430)
	at uclid.UclidMain$.executeCommands(UclidMain.scala:482)
	at uclid.UclidMain$.$anonfun$main$1(UclidMain.scala:171)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.UclidMain$.main(UclidMain.scala:171)
	at uclid.UclidMain$.main(UclidMain.scala:62)
	at uclid.UclidMain.main(UclidMain.scala)

Issue 2

Assigning a record literal to a global variable causes an assertion error within uclid.

Minimal example

module main {
    type rec_t = record { f1 : integer, f2 : bv32 };

    var state : rec_t;

    init { } 

    next {
        state' = { 100, 100bv32 };
    }   

    control {
        bmc_noLTL(5);
        check;
    }   
}

Running this file with uclid -X gives the following output:

Successfully instantiated 1 module(s).
[Assertion Failure]: Operands to '=' must of the same type. Got: record [f1 : Int, f2 : (_ BitVec 32)] tuple [Int, (_ BitVec 32)]
uclid.Utils$AssertionError: Operands to '=' must of the same type. Got: record [f1 : Int, f2 : (_ BitVec 32)] tuple [Int, (_ BitVec 32)]
	at uclid.Utils$.assert(Utils.scala:54)
	at uclid.smt.Operator.checkAllArgsSameType(SMTLanguage.scala:205)
	at uclid.smt.Operator.checkAllArgsSameType$(SMTLanguage.scala:200)
	at uclid.smt.BoolResultOp.checkAllArgsSameType(SMTLanguage.scala:439)
	at uclid.smt.EqualityOp$.typeCheck(SMTLanguage.scala:516)
	at uclid.smt.OperatorApplication.<init>(SMTLanguage.scala:854)
	at uclid.SymbolicSimulator.$anonfun$renameStates$2(SymbolicSimulator.scala:1053)
	at scala.collection.TraversableLike.$anonfun$map$1(TraversableLike.scala:273)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at scala.collection.TraversableLike.map(TraversableLike.scala:273)
	at scala.collection.TraversableLike.map$(TraversableLike.scala:266)
	at scala.collection.immutable.List.map(List.scala:298)
	at uclid.SymbolicSimulator.renameStates(SymbolicSimulator.scala:1048)
	at uclid.SymbolicSimulator.$anonfun$symbolicSimulate$1(SymbolicSimulator.scala:1130)
	at scala.collection.immutable.Range.foreach$mVc$sp(Range.scala:158)
	at uclid.SymbolicSimulator.symbolicSimulate(SymbolicSimulator.scala:1120)
	at uclid.SymbolicSimulator.prove$1(SymbolicSimulator.scala:228)
	at uclid.SymbolicSimulator.$anonfun$execute$6(SymbolicSimulator.scala:246)
	at uclid.SymbolicSimulator.$anonfun$execute$6$adapted(SymbolicSimulator.scala:236)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.SymbolicSimulator.execute(SymbolicSimulator.scala:236)
	at uclid.UclidMain$.execute(UclidMain.scala:430)
	at uclid.UclidMain$.executeCommands(UclidMain.scala:482)
	at uclid.UclidMain$.$anonfun$main$1(UclidMain.scala:171)
	at scala.collection.immutable.List.foreach(List.scala:392)
	at uclid.UclidMain$.main(UclidMain.scala:171)
	at uclid.UclidMain$.main(UclidMain.scala:62)
	at uclid.UclidMain.main(UclidMain.scala)