Correct endianness of AIGER model parsing

Includes test used to identify the bug.

intTests/test_external_abc/test.saw

@@ -39,6 +39,13 @@ write_verilog "write_verilog_seqt.v" seqt;
 let tupt = {{ \(x:[8]) (y:[8]) -> (x + y, x - y) }};
 write_verilog "write_verilog_tupt.v" tupt;
 
+let order_term = {{ \(x:[2][2][8]) -> \(y:[32]) -> y == 0x81050fff /\ x == [[2,3],[4,5]] }};
+let order_res = {{ ([[0x02,0x03],[0x04,0x05]], 0x81050fff) }};
+
 // Check that Verilog counterexamples are in the right order
-sr <- sat w4_abc_verilog {{ \(x:[2][2][8]) -> \(y:[32]) -> y == 0x81050fff /\ x == [[2,3],[4,5]] }};
-caseSatResult sr undefined (\t -> prove_print yices {{ t == ([[0x02,0x03],[0x04,0x05]], 0x81050fff) }});
+sr1 <- sat w4_abc_verilog order_term;
+caseSatResult sr1 undefined (\t -> prove_print yices {{ t == order_res }});
+
+// Check that AIGER counterexamples are in the right order
+sr2 <- sat w4_abc_aiger order_term;
+caseSatResult sr2 undefined (\t -> prove_print yices {{ t == order_res }});

src/SAWScript/Prover/ABC.hs

@@ -128,25 +128,25 @@ w4AbcExternal exporter argFn unints _hashcons goal =
        let stats = solverStats "abc_verilog" (propSize goal)
        res <- if all isSpace cexText
               then return Nothing
-              else do bits <- parseAigerCex cexText
-                      case liftLECexBB argTys bits of
+              else do cex <- liftIO $ parseAigerCex cexText argTys
+                      case cex of
                         Left parseErr -> fail parseErr
                         Right vs -> return $ Just model
                           where model = zip argNames (map toFirstOrderValue vs)
        return (res, stats)
 
-parseAigerCex :: String -> IO [Bool]
-parseAigerCex text =
+parseAigerCex :: String -> [FiniteType] -> IO (Either String [FiniteValue])
+parseAigerCex text tys =
   case lines text of
     -- Output from `write_cex`
     [cex] ->
       case words cex of
-        [bits] -> mapM bitToBool (reverse bits)
+        [bits] -> liftCexBB tys <$> mapM bitToBool bits
         _ -> fail $ "invalid counterexample line: " ++ cex
     -- Output from `write_aiger_cex`
     [_, cex] ->
       case words cex of
-        [bits, _] -> mapM bitToBool bits
+        [bits, _] -> liftLECexBB tys <$> mapM bitToBool bits
         _ -> fail $ "invalid counterexample line: " ++ cex
     _ -> fail $ "invalid counterexample text: " ++ text
   where